Abstraccion por Predicados para Especificaciones DynAlloy Expositor: Raul Fervari

Lunes 27 de septiembre de 2010, 14 hs.

DynAlloy es una extensión del lenguaje de especificación Alloy, que permite modelar de manera más apropiada propiedades de ejecución de los sistemas de software. DynAlloy provee un soporte completamente automático para la verificación de propiedades de programas, por medio de una busqueda exhaustiva de contraejemplos con dominios acotados. Pero al utilizar mecanismos algorítmicos de verificación, nos encontramos con el problema de la explosión combinatoria de estados, haciendo el análisis imposible para pequeñas cotas. Es por eso, que se presenta un enfoque para lidiar con este problema: Abstracción por Predicados.

La Abstracción por Predicados nos permite incrementar significativamente las cotas de los dominios y de iteraciones en el análisis, y su uso es completamente automático. La implementación de esta técnica es relativamente eficiente, explotando el uso de cálculos previos y realizando la verificación de propiedades bajo demanda sobre la construcción de las trazas abstractas. Además se presentará una técnica de refinamiento de abstracciones para el caso en el que nos encontramos con contraejemplos espúreos, es decir, que violan la propiedad en el modelo abstracto pero que no lo hacen en el concreto. Se presentarán las ideas principales de estos temas, como así también algunos resultados experimentales.

Video de la charla Presentación

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.