Research

Towards Secure Distributed Computations

Nowadays, there are plenty of networks that work in a cooperative way and form what we know as grids of computers. These grids are serving a lot of purposes, and they are used with good results for intensive calculation, because the joined computing power aids in solving complex functions. To cope with these new requirements and facilities, programming languages have had to evolve to new paradigms, including facilities to do distributed computing in a straightforward way.

Continue reading

Certified autonomic mechanisms for mobile security

This project targets the design of (certified) mechanisms able to proactively understand the behaviour of platforms that deploy technologies for mobile devices in order to detect/prevent vulnerable states of those platforms. To that end we aim at integrating the use of formal security models and certified proofs of properties that may be used to enforce or violate security policies with methods and techniques capable of collecting and analyzing information residing in mobile devices as well as the events that provoke creation, modification and (potentially unsecure) flow of that information.

Continue reading

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

AKD: Autonomic Knowledge Discovery for Security Vulnerability Prevention in Self-governing Systems

AKD: Autonomic Knowledge Discovery for Security Vulnerability Prevention in Self-governing Systems Nowadays, computer vulnerabilities constitute one of the main entry points for security attacks, and therefore, vulnerability management mechanisms are crucial for any computer system. On the other hand, the paradigm of autonomic computing is increasingly gaining traction as a novel model for managing complex systems and networks. Previous scientific contributions have dealt with autonomic mechanisms for assessing and remediating vulnerabilities.

Continue reading