Foundational Proof-Carrying Code and System Software

"We need firm control of the lowest-level software! [king06]"

Modular Certification of Bytecode and Intermediate Representation

Bytecode is a kind of interpretive execution instruction and a favorable intermediate representation, which is widely used in network software and mass device. The work of certifying Bytecode and related IR can highly improve the reliability of relevant software and strongly support the construction of proof-preserved compiler, so it is of important theoretical value and practical value. Although some efforts have been made on building logic system for bytecode program, modular certification of bytecode still remains challenging because of the complexity of abstract control stack and the lack of control flow structure information. Our work focused not only on the solution for certifying Bytecode which is run on stack-based virtual machine but also on the significant improvement for the construction of proof-preserved compiler environment.

What we have done:

1. DONG Yuan, WANG Shengyuan, ZHANG Liwei, ZHU Yumin and YANG Ping, A Logic System for Bytecode Modular Certification (In Chinese). Journal of Software, Vol.21, No.12, 3056−3067, 2010.
2. DONG Yuan, REN Kai, Shengyuan Wang, and ZHANG Suqin, Construction and Certification of A Bytecode Virtual Machine (In Chinese). Journal of Software. Vol.21, No.2, 305−317, 2010.
3. DONG Yuan, REN Kai, Shengyuan Wang, and ZHANG Suqin, Certify Once, Trust Anywhere -- Modular Certification of Bytecode Programs for Certified Virtual Machine. APLAS2009 (To be appeared). Seoul, Korea 14-16 December 2009.
4. DONG Yuan, WANG Shengyuan, ZHANG Liwei and YANG Ping, Modular Certification of Low-level Intermediate Representation Programs. in Proc. IEEE COMPSAC2009, Seattle, Washington, July 20-24, 2009.

Foundational Proof-Carrying Code Method for Certifying Hypervisor Low-level Codes

A hypervisor (VMM, Virtual Machine Monitor) is a virtualization platform that allows multiple operating systems to run on a host computer at the same time. It is widely used as one of the trusted computational bases to guarantee complete isolation between the virtual machines (VMs, or guest OSes) running above it, but the quality of today's main-stream hypervisors is not sufficient for safety-critical and security-critical situation. Our work aims at a novel Hoare-logic-like foundational proof-carrying code framework for certifying hypervisor low-level codes. These codes involve many features such as: stack based control, first class code point and hardware interrupts. Carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we will try to provide a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified hypervisor.

What we have done:

1. Software prototype, a small hypervisor called TinyRG: "TinyRG" which runs on 16bit real mode x86.
2. Xinyu Feng, Zhong Shao, Yuan Dong and Yu Guo, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proc. 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, Arizona, pages 170-182, June 2008. ACM
3. Xinyu Feng, Zhong Shao, Yu Guo and Yuan Dong, Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Toronto, Canada, October 2008. Springer-Verlag.
4. Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads, Journal of Automated Reasoning, 2009, 42(2-4): 301 - 347.