High-Level Program Properties in Frama-C: Definition, Verification and Deduction

In deductive verification of software, a contract is typically associated to each function and the implementation is shown to respect it. Such contracts for C programs can be expressed in the ACSL specification language. However, high-level (or global) program properties, in particular security properties, cannot be conveniently expressed as function contracts. This paper provides an overview of recent efforts to specify and verify global program properties in the Frama-C verification platform using a dedicated Frama-C plug-in called MetAcsl. Its verification approach relies on a translation of high-level properties into low-level ACSL annotations inserted in relevant program locations, followed by the verification of the resulting annotations. While this approach is expressive and powerful—and has already been effectively used in industrial applications—it can also be costly in terms of the number of the resulting low-level annotations. Deduction of high-level properties from other ones and from other annotations is thus desired. We discuss initial work on deduction of high-level properties and outline further research perspectives in this area.