SRL Projects
Current Work
There are three active projects going on in SRL at the moment:
BitC
BitC is a systems programming language designed for verifiability. Like C, BitC provides fine-grain control over data structure layout and representation. Like Standard ML, BitC has a precisely specified semantics, which allows us to reason formally about what programs written in BitC mean.
BitC also provides direct support within the language for stating theorems and invariants about the program. The value of this emerged from our group's experience with the MOPS static checker, but we wanted stronger analysis tools than MOPS could provide.
Coyotos
Coyotos is the successor to the EROS operating system. The goals of the project are to correct some of the shortcomings of the EROS design, demonstrate that an atomic kernel can scale up as well as down, provide an efficient Linux compatibility environment, and develop the proving technology necessary to formally verify key properties of the Coyotos kernel and its core system programs.
OpenCM
OpenCM is a secure, high-integrity replacement for CVS. While not as ``feature rich'' as CVS, it supports some useful things the CVS lacks, such as proper support for branching, merging, renaming, and accountability.
HDTrans
HDTrans is a general purpose dynamic translation system designed to support runtime code analysis. We are currently using it to investigate penetration resistence on binary programs at run-time.
HDTrans 0.4 has been released under the BSD copyright. The source code for HDTrans is now available. A paper describing this system appeared at the 2005 Workshop on Binary Instrumentation and Applications. A second paper appeared at VEE 2006.
Past Efforts
EROS
The EROS EROS operating system is the first high-performance capability-based operating system to execute on commodity hardware. It demonstrated both the formal and the practical feasibility of software capability operating systems. Based on what we learned in that project, we have now started work on its successor: Coyotos.