| |
|
| |
|
Zhaozhong Ni
Yale University
Modular Machine Code Verification
May 2, 2006 10:00am
Abstract:
Safety and efficiency are two highly desirable goals for software systems.
Unfortunately, under the current programming practice, they are difficult to achieve at the same time. This is especially true for system software.
Despite the progress made on safe languages and tools, a large and critical portion of software, such as OS kernels, is still written in unsafe languages. One major reason is the lack of verification theories and tools that can handle the expressive power of low-level code in a modular fashion.
In particular, many higher-order programming features, such as embedded code pointer, are very difficult to handle in expressive low-level verification.
In this talk, I will present XCAP, a logic-based proof-carrying code framework for modular machine code verification. I will explain in detail why embedded code pointer is a non-trivial problem and show how XCAP extends the original CAP (certified assembly programming) to solve the problem. I will also show how XCAP supports other non-trivial features such as impredicative polymorphisms, general references, and recursive specifications. I will then use a mini thread library written in x86 assembly to demonstrate how to certify OS-kernel level code in XCAP. I will also present a type-preserving translation from a typed assembly language to XCAP, which demonstrates how to connect XCAP to existing higher-level verification systems.
Bio:
Zhaozhong Ni is a Ph.D. candidate in the Computer Science Department at Yale University, where he is advised by Professor Zhong Shao. He received his bachelor's degree in computer science and technology from Tsinghua University, Beijing in 2000. His research interests include programming languages and systems, language-based security, type and logic systems for low-level program verification, certified operating systems, and verification of concurrency and multithreading
If you have questions, or would like to meet the speaker, please contact Ponda at 4-1994 or pondabarnes@tti-c.org. For information on future TTI-C talks or events, please go to the TTI-C Events page.