********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle S16, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 30 novembre 2007, 14h00-15h00 ************************* On Scalable Shape Analysis Hongseok Yang, Queen Mary, University of Londo Re'sume' : Shape analysis is a precise form of pointer analysis, which can be used to verify deep properties of data structures such as whether or not they are cyclic,whether they are nested, etc. Shape analyses are also expensive, and the tremendous number of abstract states they generate is an impediment to their use in verification of sizeable programs. In this talk, I will describe the techniques for improving the scalability of shape analyses. With these techniques, we have improved our analysis that was able to handle programs of up to 1,000 lines, such that it can now analyze programs of up to 10,000 lines. Our experiments also show that the new analysis is precise. It identifies memory safety errors and memory leaks in several Windows and Linux device drivers and, after these bugs are fixed, it automatically proves integrity of pointer manipulation for these drivers. This order of magnitude improvement in sizes of programs verified is obtained by combining several ideas. One is the local reasoning idea of separation logic, which reduces recomputation of analysis of procedure bodies, and which allows efficient transfer functions for primitive program statements. Another is an interprocedural analysis algorithm which aggressively discards intermediate states. The most important new technical contribution of the work is a new join (or widening) operator, which greatly reduces the number of abstract states used by the analysis while not greatly reducing precision; the join is also integrated with procedure summaries in an interprocedural analysis. This is joint work with Oukseh Lee, Cristiano Calcagno, Dino Distefano and Peter O'Hearn. *** Vendredi 30 novembre 2007, 15h00-16h00 ************************* Fighting Crime With Geometry or Automatically Proving the Absence of Buffer Overflow Vulnerabilities Axel Simon (ENS) Re'sume'/Abstract: A buffer overflow in a C program occurs when input is written into a memory buffer whose length exceeds that of the buffer. Overflows usually lead to crashes but may even allow a malicious person to gain control over a computer system. They are recognised as one of the most widespread forms of security vulnerability. In this talk I describe a static analysis for detecting buffer overflows. The analysis is conservative in the sense that it locates every possible overflow. Furthermore, it is fully automatic in that it requires no user annotations in the input program. The key idea of the analysis is to infer a concise description for each program point that over-approximates the possible variable valuations that can arise at that program point. These descriptions consist of finite sets of linear inequalities whose geometric interpretation in the form of polyhedra induce the possible variable valuations. In this talk I describe how program operations are mapped to operations on polyhedra and detail how to restrict the analysis to those portions of structures and arrays that are relevant for verification. With respect to the verification of programs that operate on string buffers, we demonstrate how to analyse C strings whose length is determined by a \NUL character in the string. ********************************************************************* Pour recevoir l'annonce par courrier electronique: WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************