Formalization

Formally verified countermeasures against cache based attacks in virtualization platforms

Cache based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time implementations, which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are protected against concurrent cache attacks in virtualization platforms; moreover, many prominent implementations are not constant-time.

Continue reading

VirtualCert

Abstract In this project we focus on the security of computer virtualization platforms. In particular, the main objective is to develop a formal idealized model of one such platform, establish non-interference security properties that should be guaranteed by the modeled control access mechanisms and to construct mathematical proofs, verified with the help of the Coq proof assistant, that those properties are verified by the model. The project has been partially funded by a grant Fondo Clemente Estable 2009 of the Uruguayan National research agency ANII and currently by a CSIC grant for R&D Projects - edition 2012.

Continue reading