Reliable and Secure Software through Static Verification and Dynamic Checking

Gang Tan
Princeton University


In this talk, I will present two projects whose goals are to achieve reliable and secure software systems. The first project is the Foundational Proof-Carrying Code. Proof-Carrying Code (PCC) statically type checks the safety of machine-language programs. But the problem is who will verify the type checker itself? The FPCC project at Princeton verifies the soundness of the type checker from the smallest possible set of axioms --- logic plus machine semantics. One challenge in the verification is that machine code, unlike high-level languages, contains unstructured control flow (due to arbitrary jumps). To address this problem, I present a program logic, L_c, which structurally verifies properties of unstructured machine code. I have built a version of L_c based on SPARC machine language and constructed machine-checked soundness proof for it. I have also proved the soundness of typing rules in FPCC from the rules in L_c. Thus with high confidence, we can check that the output of our certifying compiler is safe. The second project is the Safe Java Native Interface (SafeJNI). Java Native Interface (JNI) allows type-safe Java code to interact with unsafe C code. When a type-safe language interacts with an unsafe language in the same address space, the application becomes unsafe. I have identified the loopholes specific to using JNI that would permit C code to bypass the type safety of Java. I have designed and implemented a system that makes calling native methods in C as type-safe as pure Java code, with a moderate performance overhead.