on April 21, 2016 at 1:00 pm
Sound static analysis of C code is difficult. This talk explores the use of a C verifier as an interpreter, sacrificing soundness but eliminating imprecision due to overapproximation. This mode of analysis works best for systems that have very thorough test suites, whether manually constructed or generated by a tool such as afl-fuzz. Using Frama-C as an interpreter, we have analyzed widely-used, security-critical libraries such as SQLite, libpng, and libwebp, finding a number of issues in each and also paving the way for future sound verification efforts.
CV : Professor Regehr received his PhD in 2001 from the University of Virginia. He is currently a professor of computer science at the University of Utah, where he has been on the faculty since 2003. His research is on compilers, software testing, and software verification.
Amphithéâtre IRCICA
français
English