Availability:

• Published paper
• Slides
• Source code

Abstract.

As service providers are moving to the cloud, users are forced to provision sensitive data to the cloud. Confidential computing leverages hardware Trusted Execution Environment (TEE) to protect data in use, no longer requiring users’ trust to the cloud. The emerging service model, Confidential Computing as a Service (CCaaS), is adopted by service providers to offer service similar to the Function-as-a-Serivce manner. However, privacy concerns are raised in CCaaS, especially in multi-user scenarios. CCaaS need to assure the data providers that the service does not leak their privacy to any unauthorized parties and clear their data after the service.

To address such privacy concerns with security guarantees, we first formally define the security objective, Proof of Being Forgotten (PoBF), and prove under which security constraints PoBF can be satisfied. Then, these constraints serve as guidelines in the implementation of the PoBF-compliant Framework (PoCF). PoCF consists of a generic library for different hardware TEEs, CCaaS prototype enclaves, and a verifier to prove PoBF-compliance. PoCF leverages Rust’s robust type system and security features, to construct a verified state machine with privacy-preserving contracts. Last, the experiment results show that the protections introduced by PoCF incur minor runtime performance overhead.

BibTeX Record:

@inproceedings{chen23verify,
    author    = "Hongbo Chen and Haobin Hiroki Chen and Mingshen Sun and Kang Li and Zhaofeng Chen and XiaoFeng Wang",
    title     = "{A Verified Confidential Computing as a Service Framework for Privacy Preservation}",
    booktitle = "Proceedings of the 32nd USENIX Security Symposium",
    series    = "USENIX Security '23",
    year      = "2023",
}

Availability:

• Published paper
• Source code

Abstract.

Rust is a promising system-level programming language that can prevent memory corruption bugs using its strong type system and ownership-based memory management scheme. In practice, programmers usually write Rust code in conjunction with other languages such as C/C++ through Foreign Function Interface (FFI). For example, many notable projects are developed using Rust and other programming languages, such as Firefox, Google Fuchsia OS, and the Linux kernel. Although it is widely believed that gradually re-implementing security-critical components in Rust is a way of enhancing software security, however, using FFI is inherently unsafe. In this paper, we show that memory management across the FFI boundaries is error-prone. Any incorrect use of FFI may corrupt Rust’s ownership system, leading to memory safety issues. To tackle this problem, we design and build FFIChecker, an automated static analysis and bug detection tool dedicated to memory management issues across the Rust/C FFI. We evaluate our tool by checking 987 Rust packages crawled from the official package registry and reveal 34 bugs in 12 packages. Our experiments show that FFIChecker is a useful tool to detect real-world cross-language memory management issues with a reasonable amount of computational resources.

BibTeX Record:

@inproceedings{li22ffichecker,
    author    = "Zhuohua Li and Jincheng Wang and Mingshen Sun and John C.S. Lui",
    title     = "{Detecting Cross-Language Memory Management Issues in Rust}",
    booktitle = "Proceedings of the 27th European Symposium on Research in Computer Security",
    series    = "ESORICS '22",
    year      = "2022",
}

Availability:

• Published paper
• Website

Abstract.

Internet of Things (IoT) services are gaining increasing popularity, and IoT devices are widely deployed at many smart homes. Among all the IoT communication protocols, Zigbee is a dominant one used by billions of devices and customers. However, the design of Zigbee has not been carefully evaluated and could be exploited by attackers. In this paper, we focus on Zigbee’s network rejoin procedure, which aims to allow devices to automatically recover their network status when they accidentally go offline. We develop an automated verification tool Verejoin to perform a systematic study on the rejoin procedure. Using this tool, we not only confirm a well-known design flaw, but also reveal two undiscovered design flaws. Moreover, we construct four proof-of-concept (PoC) attacks to exploit these design flaws. These vulnerabilities create new attack surfaces for attackers to manipulate Zigbee devices, and the damage of these vulnerabilities ranges from denial of service to device hijacking. We further design a Zigbee testing tool ZigHomer to confirm these vulnerabilities in real-world devices. Using ZigHomer, we conduct thorough evaluations of off-the-shelf Zigbee devices from leading IoT vendors, and the evaluation result shows the prevalence and severity of these vulnerabilities. Finally, we reported our findings to related parties, and they all acknowledged the significant security impact. We further collaborate with Zigbee Alliance to amend the Zigbee specification, and successfully addressed our reported vulnerabilities

BibTeX Record:

@inproceedings{wang22zigbee,
    author    = "Jincheng Wang and Zhuohua Li and Mingshen Sun and John C.S. Lui",
    title     = "{Zigbee's Network Rejoin Procedure for IoT Systems: Vulnerabilities and Implications}",
    booktitle = "Proceedings of the 25th International Symposium on Research in Attacks, Intrusions and Defenses",
    series    = "RAID '22",
    year      = "2022",
}

Availability:

• Published paper
• Source code

Abstract.

Safe system programming is often a crucial requirement due to its critical role in system software engineering. Conventional low-level programming languages such as C and assembly are efficient, but their inherent unsafe nature makes it undesirable for security-critical scenarios. Recently, Rust has become a promising alternative for safe system-level programming. While giving programmers fine-grained hardware control, its strong type system enforces many security properties including memory safety. However, Rust’s security guarantee is not a silver bullet. Runtime crashes and memory-safety errors still harass Rust developers, causing damaging exploitable vulnerabilities, as reported by numerous studies.

In this paper, we present and evaluate MirChecker, a fully automated bug detection framework for Rust programs by performing static analysis on Rust’s Mid-level Intermediate Representation (MIR). Based on the observation of existing bugs found in Rust codebases, our approach keeps track of both numerical and symbolic information, detects potential runtime crashes and memory-safety errors by using constraint solving techniques, and outputs informative diagnostics to users. We evaluate MirChecker on both buggy code snippets extracted from existing Common Vulnerabilities and Exposures (CVE) and real-world Rust codebases. Our experiments show that MirChecker can detect all the issues in our code snippets, and is capable of performing bug finding in real-world scenarios, where it detected a total of 33 previously unknown bugs including 16 memory-safety issues from 12 Rust packages (crates) with an acceptable false-positive rate.

BibTeX Record:

@inproceedings{li21mirchecker,
    author    = "Zhuohua Li and Jincheng Wang and Mingshen Sun and John C.S. Lui",
    title     = "{MirChecker: Detecting Bugs in Rust Programs via Static Analysis}",
    booktitle = "Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security",
    series    = "CCS '21",
    year      = "2021",
}

Availability:

• Published paper
• Source code

Abstract.

In the past decade, Trusted Execution Environment (TEE) provided by ARM TrustZone is becoming one of the primary techniques for enhancing the security of mobile devices. The isolation enforced by TrustZone can protect the trusted applications running in the TEE against malicious software in the untrusted rich execution environment (REE). However, TrustZone cannot completely prevent vulnerabilities in trusted applications residing in the TEE, which can then be used to attack other trusted applications or even the trusted OS. Previously, a number of memory corruption vulnerabilities have been reported on different TAs, which are written in memory-unsafe languages like C.

Recently, various memory-safe programming languages have emerged to mitigate the prevalent memory corruption bugs. In this paper, we propose RusTEE, a trusted application mechanism that leverages Rust, a newly emerged memory-safe language, to enhance the security of TAs. Though the high-level idea is quite straight-forwarding, we resolve several challenges on adopting Rust in mobile TEEs. Specifically, since Rust currently does not support any TrustZone-assisted TEE systems, we extend the existing Rust compiler for providing such support. Also, we apply comprehensive security mechanisms to resolve two security issues of trusted applications, namely, securely invoking high-privileged system services and securely communicating with untrusted REE. We implement a prototype of RusTEE as the trusted applications’ SDK, which supports both emulator and real hardware devices. The experiment shows that RusTEE can compile applications with close-to-C performance on the evaluated platforms.

BibTeX Record:

@inproceedings{wan20rustee,
    author    = "Shengye Wan and Mingshen Sun and Kun Sun and Ning Zhang and Xu He",
    title     = "{RusTEE: Developing Memory-Safe ARM TrustZone Applications}",
    booktitle = "Proceedings of the 36th Annual Computer Security Applications Conference",
    series    = "ACSAC '20",
    year      = "2020",
    month     = "12",
}

Availability:

• Published paper

Abstract. Intel Software Guard eXtension (SGX), a hardware supported trusted execution environment (TEE), is designed to protect security critical applications. However, it does not terminate traditional memory corruption vulnerabilities for the software running inside enclave, since enclave software is still developed with type unsafe languages such as C/C++. This paper presents RUST-SGX, an efficient and layered approach to exterminating memory corruption for software running inside SGX enclaves. The key idea is to enable the development of enclave programs with an efficient memory safe system language Rust with a RUST-SGX SDK by solving the key challenges of how to (1) make the SGX software memory safe and (2) meanwhile run as efficiently as with the SDK provided by Intel. We therefore propose to build RUST-SGX atop Intel SGX SDK, and tame unsafe components with formally proven memory safety. We have implemented RUST-SGX and tested with a series of benchmark programs. Our evaluation results show that RUST-SGX imposes little extra overhead (less than 5% with respect to the SGX specific features and services compared to software developed by Intel SGX SDK), and meanwhile have stronger memory safety.

BibTeX Record:

@inproceedings{wang2019towards,
    author    = {Wang, Huibo and Wang, Pei and Ding, Yu and Sun, Mingshen and Jing, Yiming and Duan, Ran and Li, Long and Zhang, Yulong and Wei, Tao and Lin, Zhiqiang},
    title     = {Towards Memory Safe Enclave Programming with Rust-SGX},
    booktitle = {Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security},
    series    = {CCS '19},
    year      = {2019},
} 

English

Recently, we first announced the MesaPy project, which aims to be a fast and safe Python implementation. MesaPy mainly focuses on improving its security and memory safety. 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 three 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.

On top of the enhancements, we also bring MesaPy into Intel SGX to write memory-safe applications running in the trusted execution environment. Intel SGX provides integrity and confidentiality guarantees to security-sensitive computation. Developers now can easily use MesaPy for SGX to implement SGX applications (SGX enclaves) without worrying about memory issues and with minimal TCB (Trusted Computing Base).

Building a Python enclave is quite simple, and we provide several examples to show the capabilities. Let’s take “Hello World” as an example. Firstly, developers need a machine with SGX support, install with Intel SGX PSW/SDK, and its dependencies. Then, clone the MesaPy for SGX repository.

$ git clone -b sgx --recursive git@github.com:mesalock-linux/mesapy.git

Secondly, build MesaPy for SGX in the sgx directory.

$ make sgx    # build MesaPy for SGX

After successfully building MesaPy for SGX, you can start the “Hello World” project finally.

$ source $(SGX_SDK)/environment  # setup Intel SGX SDK environment variables
$ cd sgx/examples/hello_world    # change to the hello_world directory
$ make                           # compile, link and sign the enclave
$ ./app                          # run the enclave and get the "Hello, World!" message
Hello, World!
Welcome to MesaPy for SGX.
Do what I mean: 42

Info: hello_world successfully returned.
Enter a character before exit ...

To write a customized Python enclave, developers can just modify the Enclave/src/python_enclave.py file. Detailed instructions are described in the README file. In addition, we also provide Dockerfile to ease the developing process.

Because of security concerns, MesaPy for SGX is not designed as a general purpose Python interpreter for SGX. That is, some full-fledged libraries and modules can not be used in MesaPy for SGX without any modifications.

Currently, MesaPy for SGX supports Python 2 syntax and most built-in functions. For the standard library, it supports these modules (because dynamic module importing is an ongoing feature, more modules will be supported when it's done):

• essential modules: exceptions, _file, sys, __builtin__, _warnings, itertools,
• default modules: __pypy__, marshal, operator, _ast, _weakref, _cffi_backend
• additional working modules: _codecs, gc, _weakref, marshal, errno, imp, math, cmath, _sre, _pickle_support, operator, parser, symbol, token, _ast, _io, _random, __pypy__, _testing, cStringIO, struct, array, binascii, itertools, _md5, _sha, _collections, micronumpy, _cffi_backend, _pypyjson.

The modules may be updated in the future, and the full list can be found at the pypy/config/pypyoption.py file. We also test these modules in SGX in the sgx/tests directory.

In the current release, MesaPy for SGX supports basic computation and some builtin modules. Supports of multithreading, GC and the standard library are still under developing. The project is open source in GitHub. If you are interested in contributing to MesaPy for SGX, feel free to open an issue with your plan and start working on it.

中文

我们首次公布了 MesaPy 开源项目，致力提供一个内存安全、运行快速的 Python。MesaPy 继承了 PyPy 优越的性能优势，并提供内存安全、安全增强、形式化验证等安全特性。本次更新迎来了又一大安全特性，就是支持 Intel SGX 可信执行环境。

MesaPy for SGX 通过对 MesaPy 的精简和对内置库的改造，使得开发者可以使用 Python 轻松的编写出 SGX 应用（Python enclave）。MesaPy for SGX 不仅加速了 SGX 应用的开发效率，保证在可信执行环境中极小的 TCB（Trusted Computing Base），同时提供内存安全的运行环境。使用 MesaPy for SGX 进行 SGX 的应用开发非常简单，我们提供了多个样例应用，只需修改样例程序，编写自定义的 Python 代码，编译执行即可。

以 “Hello World” 为例，首先开发者在支持 SGX 的机器上，安装 Intel SGX PSW/SDK 程序以及编译所需的依赖，然后克隆 MesaPy for SGX 的代码仓库：

$ git clone -b sgx --recursive git@github.com:mesalock-linux/mesapy.git

进入 sgx 目录然后编译 MesaPy for SGX:

$ make sgx    # 编译 MesaPy for SGX

编译成功后就可以通过以下命令编译执行 “Hello World” 的例子。

$ source $(SGX_SDK)/environment  # 设置 Intel SGX SDK 的环境变量
$ cd sgx/examples/hello_world    # 进入 hello_world 例子的目录
$ make                           # 编译、链接、签名 hello_world
$ ./app                          # 执行 enclave，将输出 Hello, World!
Hello, World!
Welcome to MesaPy for SGX.
Do what I mean: 42

Info: hello_world successfully returned.
Enter a character before exit ...

如需要编写自己的 Python enclave，只需要修改 Enclave/src/python_enclave.py 文件即可，README 中也有详细的介绍。同样，我们也提供了 Dockerfile，为 Python enclave 的开发提供便利。

MesaPy for SGX 现在已经支持基本的数学运算和一些内置库，对于多线程、垃圾回收、标准库的移植等开发工作仍在进行中，所有代码已开源在 GitHub 中（链接），欢迎感兴趣的朋友加入共同推进 MesaPy 对于 SGX 的支持。

Availability:

• Published paper
• Source code

Abstract. Device drivers on Linux-powered embedded or IoT systems execute in kernel space thus must be fully trusted. Any fault in drivers may significantly impact the whole system. However, third-party embedded hardware manufacturers usually ship their proprietary device drivers with their embedded devices. These out-of-tree device drivers are generally of poor quality because of a lack of code audit. In this paper, we propose a new approach that helps third-party developers to improve the reliability and safety of device drivers without modifying the kernel: Rewriting device drivers in a memory-safe programming language called Rust. Rust’s rigorous language model assists the device driver developers to detect many security issues at compile time. We designed a framework to help developers to quickly build device drivers in Rust. We also utilized Rust’s security features to provide several useful infrastructures for developers so that they can easily handle kernel memory allocation and concurrency management, at the same time, some common bugs (e.g. use-after-free) can be alleviated. We demonstrate the generality of our framework by implementing a real-world device driver on Raspberry Pi 3, and our evaluation shows that device drivers generated by our framework have acceptable binary size for canonical embedded systems and the runtime overhead is negligible.

BibTeX Record:

@inproceedings{li2019securing,
    author    = "Zhuohua Li and Jincheng Wang and Mingshen Sun and John C. S. Lui",
    title     = "{Securing the Device Drivers of Your Embedded Systems: Framework and Prototype}",
    booktitle = "Proceedings of the 14th International Conference on Availability, Reliability and Security",
    series    = {ARES '19},
    year      = {2019},
}

Availability:

• Published paper

Abstract.

Record/replay system is an essential and widely used module in forensic analysis, as it can help forensic analysts to reconstruct programs’ behaviors. However, the security implication of record/replay systems (i.e., whether record/replay systems can faithfully reproduce all behaviors of a program) has not been thoroughly studied. This paper is the first work which investigates and explores the security limitations of record/replay systems from the perspective of software forensics. In particular, we reveal a type of vulnerability in record/replay systems caused by non-uniform program execution time. A program can exploit this vulnerability to prevent its malicious behavior from being replayed. We conduct a series of experiments on three platforms (i.e., web browser, mobile operating system and virtualized sandbox) to illustrate the wide footprints of the vulnerability. Finally, we discuss possible methods to mitigate the vulnerability. The goal of this work is to study the inherent security limitations of record/replay systems, discover the vulnerability and explore potential mitigation methods, from which forensic analysts can be informed and cautious when applying record/replay systems to software forensics.

BibTeX Record:

@article{hu2019exploiting,
  title = "Exploiting non-uniform program execution time to evade record/replay forensic analysis",
  journal = "Computers & Security",
  year = "2019",
  issn = "0167-4048",
  doi = "https://doi.org/10.1016/j.cose.2019.04.012",
  author = "Yang Hu and Mingshen Sun and John C.S. Lui",
}

Availability:

• Conference slides
• Video

Abstract:

Rust is designed to be a system programming language which is fast and guarantees memory safety. However, building safe and secure systems is not simply using Rust to rewrite existing code. Still, there are many challenges such as the Rust language, unsafe Rust, foreign function interface (FFI), and designing systems with a hybrid memory model. In this talk, we will discuss some challenges in the view of security. We will demonstrate the challenges and lesson learned by using some real-world case studies. Finally, we will raise some open questions, initial ideas, and possible solutions.

BibTeX Record:

@article{sun2018building,
  author = {Sun, Mingshen},
  title = {Building Safe and Secure Systems in Rust},
  journal = {RustRush},
  year = {2018},
}