TRust is a long-term project focusing on programming languages and trusted compilation by developing formal semantics of languages and formal verification of compiling. The final goal of this project is to create a formally verified compiler for various languages.
In this project, we have created a formal programming language (CSimpl) in Isabelle/HOL. CSimpl is a generic and realistic imperative language by extending Simpl and providing a rely-guarantee proof system for compositional reasoning of concurrent programs and a refinement approach for top-down development of concurrent systems. Simpl is composed of the necessary constructs to capture most of the features present in common sequential languages, such as conditional branching, loops, abrupt termination and exceptions, assertions, mutually recursive functions, expressions with side effects, and nondeterminism. Additionally, Simpl can express memory related features like the memory heap, pointers, and pointers to functions. Simpl is able to represent a large subset of C99 code and has been applied to the formal verification of seL4 OS kernel at C code level.
In this project, we have also developed comprehensive formal semantics of LLVM IR language in Isabelle/HOL, and AADL architecture language and its verification approach in Isabelle/HOL. Using our PiCore framework and integrated languages, we have developed the formal semantics of a core subset of BPEL business process language and a verified compilation of BPEL programs to PiCore specification (see PiCore for more details ).
Developing correct concurrent systems is a large challenge. To provide a programming language and further a formal reasoning system for concurrent systems, we developed CSimpl, a generic and realistic imperative language in Isabelle/HOL theorem prover. CSimpl provides a rely-guarantee proof system for compositional reasoning of concurrent programs and a refinement approach for top-down development of concurrent systems in the correct-by-construct manner.
It is essential to deal with the interference of the environment between programs in concurrent program verification. This has led to the development of concurrent program reasoning techniques such as rely-guarantee. However, the source code of the programs to be verified often involves language features such as exceptions and procedures which are not supported by the existing mechanizations of those concurrent reasoning techniques. Schirmer et al. have solved a similar problem for sequential programs by developing a verification framework in the Isabelle/HOL theorem prover called Simpl, which provides a rich sequential language that can encode most of the features in real world programming languages. However Simpl only aims to verify sequential programs, and it does not support the specification nor the verification of concurrent programs. CSimpl is an extension of Simpl with concurrency oriented language features and verification techniques. We prove the compositionality of the CSimpl semantics and we provide inference rules for the language constructors to reason about CSimpl programs using rely-guarantee, showing that the inference rules are sound w.r.t. the language semantics.
To support compositional top-down verification of concurrent systems using rely-guarantee, we propose CSim2 a compositional rely-guarantee-based framework for complex concurrent systems in the Isabelle/HOL theorem prover. CSim2 uses CSimpl to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim2 provides a simulation based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations.
- David Sanan, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, Yang Liu, "CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs", 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, ETAPS), 22-29 April 2017, Uppsala, Sweden, pp. 481-498 (CCF B, Top conf. in formal methods) [PDF download]
- David Sanan, Yongwang Zhao#, Yang Liu, Shangwei Lin, "CSim2 : Compositional Top-down Verification of Concurrent Systems Using Rely-Guarantee", ACM Transactions on Programming Languages and Systems (TOPLAS) , to appear (CCF A, top journal in programming languages)