Research
Research Overview
Last modified: Tue Apr 17 17:28:22 2007 GMT.
The correctness of computer software is vital to the world's safety-critical systems (where software bugs can cause injury or death) and security-critical applications (where an attacker is deliberately searching for, and exploiting, software bugs). Among all the engineering disciplines, computer software is probably today's least reliable artifact widely used in our society. Every year major corporations and government agencies worldwide invest huge amounts of resources fixing software bugs, but the prospect of building reliable software remains grim. An important reason for this difficulty comes from the sheer complexity of software systems: if each line in a program is considered as an individual part, software programs are easily the most complicated things people have ever built. Nevertheless, a software program is strictly a mathematical entity; if all hardware components perform as expected, the behavior of each software program (including the underlying operating system) should be possible to rigorously specify and reason about.The FLINT group is interested in attacking the following pressing question on software reliability: "Is it possible to build certified bug-free software? If yes, how to develop new tools that would make writing certified programs easier, more scalable, and more accessible?" We intend to construct a practical infrastructure for building large-scale certified systems software, focusing on the development of integrated programming and proof tools and new program verification techniques.
Certified software consists of a machine executable plus a complete rigorous proof (also stored inside a computer) that the software is free of bugs with respect to a particular specification. Both the proof and the specification are written using a general-purpose mathematical logic, the same logic which we use (in reasoning) in our daily life. The logic is also a programming language: everything written in logic (including proofs and specifications) is developed using a software known as proof assistants; they can be mechanically checked for correctness by a small program known as proof checker. As long as the logic we use is consistent, and the specification meets what the user wants, we can be sure that the underlying software is free of bugs with respect to the specification. A developer writing certified software need to put in much more work initially since she also has to build the proof. Machine checked proofs of real software systems are difficult but are now possible given the recent advances in the theory and engineering of mechanized proof systems applied to software verification.
Software at different scale has different cost-benefits from verification. For example, software that controls the anti-lock brake system must be proved correct in the entire software-hardware stack of an automobile; software that controls the web server must be proved resistant of certain kinds of attacks; on the other hand, many large business applications would be inappropriate to be fully specified and proved correct, however, the protection mechanism of the operation system (or runtime system) in which they operate might well be proved correct to guard against the uncontrolled exchanges of data.
Certifying large software requires more powerful and integrated programming and proof tools. We will apply language-based techniques (for building large software) to make existing proof assistants more suitable for building large proofs. Both Coq and Isabelle/HOL were primarily developed for reasoning about mathematics. To use them to reason about low-level code, we must add support for general-purpose programming constructs and machine-level instructions and data types. Proofs should also be more modular and readable. We will develop a shared program logic with independent proof checker so that certified code developed for different languages, in different proof assistants, can be reused and linked together. Certified software would only be practical if the underlying core system software (e.g., operating system kernels, device drivers) are also certified. We will develop new formal frameworks (including innovative program logics and type systems) for reasoning about vanilla C and assembly programs. We will also build certified (and certifying) compilers, program verifiers, and analysis tools to support better proof automation.
If successful, the technology of building certified software will have a profound impact on the software industry and the society in general. It will dramatically improve the reliability and security of many key components in the world's critical infrastructure. It will advance the human knowledge on what is possible in building bug-free software and whether future software will ever be built on top of a reliable core. Software components with machine-checkable specifications and proofs will be easier to understand, more maintainable, and more portable.
