mesalock-linux / mesapy

A Fast and Safe Python based on PyPy

MesaPy: A Memory-Safe Python Implementation based on PyPy

English | 中文

MesaPy is a memory-safe Python implementation based on PyPy. In addition to PyPy's distinct features -- speed (thanks to the JIT compiler), memory usage, compatibility and stackless (massive concurrency), MesaPy mainly focuses on improving its security and memory safety. On top of the enhancements, we also bring MesaPy into Intel SGX to write memory-safe applications running in the trusted execution environment.

We achieve the memory-safety promise through various methods: hardening RPython's type system (RPython is the language for writing PyPy), modifying PyPy/RPython's libraries, and verifying the RPython's libraries as well as its translator/JIT backend. Overall, there are four most notable security features of MesaPy:

• Memory safety: To provide a memory-safe runtime, MesaPy replaces external libraries written in C, which could introduce memory issues, with Rust, a memory-safe programming language. This guarantees the memory safety across all libraries including those written in Python, but also external libraries.

• Security hardening: PyPy is implemented with RPython, a statically-typed language with translation and support framework. We also enhanced memory-safety of RPython through hardening RPython's type system, i.e., the RPython typer. For example, we improve RPython's list with runtime index check to avoid arbitrarily list read/write during PyPy's implementation.

• Formal verification: Some code in RPython's libraries and its translator/JIT backend are still written in C, which may contain potential memory bugs. To prove the memory safety of RPython, we aim to formally verify its libraries and backend written in C using state-of-the-art verification tools.

• SGX support: With the memory safety of MesaPy, we also port it to Intel SGX, which is a trusted execution environment to provide integrity and confidentiality guarantees to security-sensitive computation. Developers now can easily use MesaPy to implement SGX applications without worrying about memory issues.

More details about each features, roadmap, and building process can be found here: https://docs.mesapy.org/

Design

MesaPy enhances PyPy in security. Compared to CPython (also known as Python), MesaPy provides a comprehensive security protection. Following figure illustrates MesaPy's design and implementation. Blocks highlighted in red means unsafe components, while blue blocks represent safe components. MesaPy aims to protect Python runtime by our security hardening.

By using formal verification, type system enhancement, and memory safe programming language, MesaPy mitigates potential memory safety issues of both CPython and PyPy. MesaPy's goal is to provide a fast and memory safe Python runtime.

Getting Started

Basically, you can use MesaPy as any other Python implementations (e.g., CPython and PyPy). There are many ways to experience MesaPy:

• the pre-built binary of MesaPy
• use MesaLock Linux docker to try MesaPy: docker run --rm -it mesalocklinux/mesalock-linux:latest mesapy
• build MesaPy by yourself from source

Building MesaPy from source

Building MesaPy from source is very simple, you can simply use the docker provided by MesaLock Linux and run make pypy-c. The detailed steps are explained in the documentation.

$ git clone --recursive [email protected]:mesalock-linux/mesapy.git # recursively clone mesapy and its submodules
$ cd mesapy
$ docker run --rm -it -v$(pwd):/mesapy -w /mesapy mesalocklinux/build-mesalock-linux make pypy-c

Using MesaPy for SGX

One unique feature of MesaPy is to support Intel trusted execution environment -- SGX. Developers now can use Python to implement security-sensitive applications. The ultimate goal of MesaPy is to have SGX as a platform (just like x86 and arm in MesaPy). Right now, the MesaPy for SGX is under the sgx branch, so please checkout the branch first. You can follow the instruction in its README to start using MesaPy for SGX. Note that this is a work-in-progress feature, current version has limited functions and packages. Contributions are very welcome.

To run Python app in SGX is very simple:

• checkout and build MesaPy for SGX
• write Python embeddings
• use MesaPy for SGX to build an SGX enclave with the Python embeddings

We also provide some examples (under the /sgx/examples directory ) to quickly start using MesaPy for SGX. You can also read details in our documentations.

Formal verification

There are still few lines of C code left in RPython translator/JIT and its libraries which are difficult to eliminate. For these code, we still want to guarantee its memory safety, by utilizing formal verification methods. We use three state-of-the-art verification tools, Seahorn, Smack, and TIS (TrustInSoft) to prove conclusively that the memory safety issues can never occur, which includes:

• Buffer overflow
• Buffer over-read
• Null pointer dereference
• Memory leak

We have verified code in RPython translator, and the verification results are illustrated in the verification directory. We are also working on a technical report to present our findings.

The detailed instructions and additional mocks are also included in each tool's separate directory. You can easily reproduce the verification process. You are welcome to contribute mocks and help us to verify files in the TODO list.

Benchmark

We used 19 Python scripts to run our performance evaluation. Each script is executed in ten times for MesaPy, PyPy 6.0.0, and Python 2.7.12 respectively. The benchmarks are shown in the following figure.

Thanks to JIT and efficient GC mechanism, MesaPy can achieve 10x plus speedup compared to Python 2.7.12.

Contributing

We still have some working-in-progress sub-projects. We are very happy if you are interested to help out. Here are several topics you can get involved:

• porting Rust libraries into MesaPy and replacing previous external C libraries
• helping to verifying "unsafe" components using current state-of-the-art verification tools
• improving MesaPy in SGX (bringing in useful libraries in normal world into SGX)

For each topic, we provided detailed instructions to get started. Feel free to pick an interesting one and improve MesaPy and send us pull requests on the GitHub. If you find it a little difficult, you can also talk to our maintainers for help.

Acknowledgment

The MesaPy project would not have been possible without the following high-quality open source projects.

• PyPy: PyPy is a fast, compliant alternative implementation of the Python language, which provides distinct features -- speed, memory usage, compatibility, and stackless. Thanks to these amazing maintainers.

Maintainer

Thanks to our maintainers to contribute this projects. Feel free to submit issues on GitHub or send us email. We are very glad to help out.

The projects are maintained by:

• Memory-safety, security hardening, SGX, and all about MesaPy: Mingshen Sun (@mssun)
• Formal verification: Qian Feng (@qian-feng)

Also, thanks to our contributors: Huibo Wang (@MelodyHuibo)and Yu Ding (@dingelish)

Steering Committee

• Tao Wei
• Yulong Zhang

License

MesaPy is provided under the 3-Clause BSD license. MesaPy is built upon PyPy and other open source projects, see the LICENSE file for detailed licenses.

mesapy's Issues

Can't find libpypy-c.a

I built a docker and followed the steps and got

$ /mesapy/sgx/examples/hello_world# make run
MAKE <=  ../../sgx_ulibc
LINK =>  app
MAKE <=  ../../sgx_tlibc_ext
g++: error: ../../../pypy/goal/libpypy-c.a: No such file or directory
g++: error: ../../libffi/build_dir/lib/libffi.a: No such file or directory
Makefile:234: recipe for target 'enclave.so' failed
make: *** [enclave.so] Error 1

如何关闭mesapy sgx example print打印？

我的操作如下：

make sgx
source /opt/intel/sgxsdk/environment 
cd sgx/examples/hello_world
make SGX_PRERELEASE=1 SGX_DEBUG=0
./app

结果如下：

我理解say()函数是运行在SGX enclave区域的，编译方式是pre_release这种方式，print应该是无法将数据打印到普通内存的。

但是print依然可以打印到终端，是我理解有错误吗？请大神们帮忙解决下。

Random模块

mesapy 暂时不支持random模块，mesaTEE开发需要 根据比例随机划分，需要 random模块

Potential security vulnerability CVE-2018-1000802 in this repository

Potential security vulnerability in mesalock-linux/mesapy file lib-python/2.7/shutil.py

https://www.cvedetails.com/cve/CVE-2018-1000802/

I found this via https://www.deepfoss.com

mesapy 不支持生成器generator

打印 generator 或者generator中的元素，报错

Supported Python Versions

Great project! Which versions of Python are currently supported though?

I could only find Python 2.7 mentioned in the READAME which is outdated and official support soon is dropped. Supporting at least Python 3.6 would make this project interesting to a wider audience.

Support random function in sgx mesapy

mesapy的编程文档有吗？就是支持哪些矩阵操作？怎么进行操作？

JIT safety is not documented

JIT is quite perilous from the correctness and security standpoints, but this is currently not addressed in the README.

If you write an interpreter in Rust you can use rustc to guarantee memory safety, but with JIT you're essentially emitting arbitrary assembly at runtime and jumping into it. No amount of memory safety guarantees on the original code will guarantee memory safety in the generated code.

Please document how this is addressed (if at all).

P.S. Thank you for the very interesting project that's pushing the boundaries of safety as we know it!

Does this platform support sklearn？

Does this platform support sklearn？
Because most of the algorithms used are from sklearn.

Why not base on CPython?

This project is based on PyPy interpreter.
Why not put CPython to SGX? CPython is more widely used.

How to run mesapy after compilation

I successfully ran make sgx. Now, how do I run it? Where is the compiled binary?

How to add a new module?

I added a new module to pypy/module and modified https://github.com/mesalock-linux/mesapy/blob/sgx/pypy/config/pypyoption.py

After compilation, my pypy can't import the module I added. Did I miss anything?