The Research of USTC-Yale Joint Research Center for High Confidence Software
Gets Attention
Technology Review chooses top 10 emerging technologies 2011 recently, and Crash-Proof Code is one of themThis technology is a software mechanism that uses logical reasoning approach to verify program, in order to construct highly reliable safety critical software.
Technology Review mainly introduces the verification of seL4, a practical operating system kernel competed by NICTA, Australia's national IT research center, in 2009. It is proved that seL4 will run reliably,never crash, and always meet the requirements of its security properties, provided the trusted computing based, the premise of the proof, is satisfied.
The report about this technology in Technology Review mentions that other researchers working on crash-proof code are Xinyu Feng of our university,Chris Hawblitzel of Microsoft Research Redmond and Zhong Shao of Yale University, who is a Master Lecturer Professor of our university.
Professor Shao, Professor Feng and other researchers in USTC-Yale Joint Research Center for High Confidence Software also verified a small operating system in 2008. Although this kernel is just a tiny experimental system, but its function is less than seL4 and the trusted computing based is also smaller than seL4. Because it is based on a very basic meta-logic and all of the codes have been verified, but in seL4, the underlying c code and 600 lines of assembly code are not verified. The smaller the trusted computing based is, the more reliable the verification is.
USTC-Yale Joint Research Center for High Confidence Software
