International audience

Abstract The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. While Debian policy provides guidance for package maintainers producing the scripts, few tools exist to check the compliance of a script to it. We report on the application of a formal verification approach based on symbolic execution to find violations of some non-trivial properties required by Debian policy in maintainer scripts. We present our methodology and give an overview of our toolchain. We obtained promising results: our toolchain is effective in analysing a large set of Debian maintainer scripts and it pointed out over 150 policy violations that lead to reports (more than half already fixed) on the Debian Bug Tracking system.

We present a new approach to deductive program verification based on auxiliary programs called ghost monitors . This technique is useful when the syntactic structure of the target program is not well suited for verification, for example, when an essentially recursive algorithm is implemented in an iterative fashion. Our approach consists in implementing, specifying, and verifying an auxiliary program that monitors the execution of the target program, in such a way that the correctness of the monitor entails the correctness of the target. The ghost monitor maintains the necessary data and invariants to facilitate the proof. It can be implemented and verified in any suitable framework, which does not have to be related to the language of the target programs. This technique is also applicable when we want to establish relational properties between two target programs written in different languages and having different syntactic structure. We then show how ghost monitors can be used to specify and prove fine-grained properties about the infinite behaviors of target programs. Since this cannot be easily done using existing verification frameworks, we introduce a dedicated language for ghost monitors, with an original construction to catch and handle divergent executions. The soundness of the underlying program logic is established using a particular flavor of transfinite games. This language and its soundness are formalized and mechanically checked.

The JAVA CARD transaction mechanism allows to protect sensitive operations on smart cards against problems due to card tears or power losses. Statements within a transaction are viewed as a single atomic operation so that either they are all performed or none of them is. KRAKATOA is a tool for static verification of Java programs annotated in JML (Java Modeling Language), a behavioral specification language tailored to Java and based on first order predicate logic. In a first step, we show how we modeled the transactions within KRAKATOA, by generating on-the-fly (i.e. on each applet) specifications of the API methods for transactions. In a second step, we consider security problems that can be caused by a card tear. We propose new JML constructs allowing to express properties to satisfy when a method is interrupted by a card tear, also taking non-atomic methods into account. We present a modeling of these constructs in KRAKATOA, and show it is practicable for the detection of potential security holes, or to prove the absence of risk.

We describe an experiment of formal verification of C source code, using the CADUCEUS tool. We performed a full formal proof of the classical Schorr-Waite graph-marking algorithm, which has already been used several times as a case study for formal reasoning on pointer programs. Our study is original with respect to previous experiments for several reasons. First, we use a general-purpose tool for C programs: we start from a real source code written in C, specified using an annotation language for arbitrary C programs. Second, we use several theorem provers as back-ends, both automatic and interactive. Third, we indeed formally establish more properties of the algorithm than previous works, in particular a formal proof of termination is made.

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as muterm, CiME, AProVE, TTT, Termptation, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned tools.

Introduces normalised rewriting, a new rewrite relation. It generalises former notions of rewriting modulo E, dropping some conditions on E. For example, E can now be the theory of identity, idempotency, the theory of Abelian groups, or the theory of commutative rings. We give a new completion algorithm for normalised rewriting. It contains as an instance the usual AC completion algorithm (AC being the set of equations containing the associativity and commutativity axioms), but also the well-known Buchberger's algorithm for computing standard bases of polynomial ideals. We investigate the particular case of completion of ground equations. In this case, we prove by a uniform method that completion modulo E terminates, for some interesting E. As a consequence, we obtain the decidability of the word problem for some classes of equational theories. We give implementation results which show the efficiency of normalised completion with respect to completion modulo AC.>