The next D2 seminar, entitled “The Squirrel Prover”, by Charlie Jacomme, will be held on February 4 at 1:00 pm in room A008. Abstract The Squirrel Prover is a proof assistant dedicated to cryptographic protocols. It relies on a higher-order logic following the computationally complete symbolic attacker approach. It thus provides guarantees in the computational model. In this talk, we will introduce the main ingredients underlying its logic and proof system, trying to outline why it does yield computational guarantees…
Find out more »The next D2 seminar, entitled “A scalable framework for backward bounded static symbolic execution”, by Nicolas Bellec, will be held on March 4 at 1:00 pm in room A008. Abstract Many programs (e.g. malware) hide their behavior by using obfuscations such as opaque predicates. Automatic methods have been developed to detect such obfuscations. In this presentation, we will focus on static symbolic backward bounded execution, a method that enumerates backward bounded paths from a potential opaque predicate and uses symbolic…
Find out more »
