Proving security properties of programs in capability safe languages

Date: April 29, 2016
Time: 11:00 – 11:50
Location: Meeting Room Levico - Polo Scientifico e Tecnologico "Fabio Ferrari" (Edificio Povo 2, via Sommarive 9 – Povo, Trento)

Speaker 
Prof. Frank Piessens - Katholieke Universiteit Leuven, Belgium 
 
Abstract 
Object capabilities are a technique for fine‐grained privilege separation in programming languages and systems, with important applications in security. However, reasoning about the security properties of programs developed using this technique is non‐trivial. 
This talk discusses a novel approach to formally reason about the security properties of programs in capability safe languages. The approach uses (and extends) state‐of‐the‐art techniques from programming languages research, and is powerful enough to reason about typical object capability patterns.

About the speaker 
Frank Piessens is a professor in the Department of Computer Science at the Katholieke Universiteit Leuven, Belgium. His research field is software security, where he focuses on the development of high‐assurance techniques to deal with implementation‐level software vulnerabilities and bugs, including techniques such as software verification, run‐time monitoring, type systems and programming language design. He studies the theory behind these techniques as well as their application in many types of software systems, including web applications, embedded software, and mobile applications.  
His contributions to the field of software security include the development of verification techniques for C‐like languages, the development of the secure multi‐execution technique for enforcing information flow security, and the development of a variety of countermeasures for buffer overflow style vulnerabilities.

Contact person regarding this talk: Fabio Massacci, fabio.massacci [at] unitn.it