Assurance and Verification of Security Properties

ABSTRACT. This paper reviews the results of our recent research in assurance and verification of embedded software systems. This research was part of an effort in which we prepared evidence, including an abstract formal model and mechanical proofs, of the security of an embedded system implemented in the C language. It then describes the evidence provided for the certification and how this evidence might be presented in an assurance case The paper also describes our more recent research on SecProve, a tool for automatically checking the security of C programs during their development. It concludes by listing some open research problems in system assurance and verification.