Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations

Expositor: Felipe Manzano

Lunes 13 de Septiembre de 2009, 14 hs.

We develop an extension of standard symbolic execution to tackle the analysis of code that uses black box functions like cryptographic primitives. Our extension treats such primitives as symbolic terms that can be rewritten and simplified within an equational theory. Our code runs in a (simplified) LLVM virtual machine. We develop concrete and symbolic semantics for our LLVM, and show our approach sound by proving operational correspondence between the two semantics. We develop a prototype and illustrate the usefulness of our approach with several (sequential code) examples, and discuss next milestones towards symbolically analysing fully concurrent cryptographic protocol implementations.

Video de la charla Presentación

Rule Formats for Non Interference

Expositor: Matias Lee http://www.matiaslee.com.ar

Lunes 17 de Mayo, 17hrs en la Sala Smith (tercer piso)

En un sistema multinivel, usuarios de distintos niveles manejan información con distintos niveles de seguridad. En este contexto, un sistema es seguro si un usuario de bajo nivel no puede interferir en el funcionamiento de un nivel superior u obtener información de este. Esta idea de formaliza con el concepto de non-interferencia. En esta charla presentaremos distintas formalizaciones de ésta. Además, presentaremos formatos de reglas para especificar sistemas de transición que nos garantizan que los sistemas obtenidos satisfacen la propiedad de interés.