I supervise Elisabet on fundational aspects of security and mechanised security proofs.
I supervise Marco on developing secure functional languages with emphasis on obtaining mechanised security proofs.
I supervised Luciano on taint analysis for the Python Google App Engine. This project was supported by a Google Research Award.
Now at IBM T.J. Watson
I supervise Pablo on applying functional languages to protect confidentiality in Haskell programs.
I supervised Deian on securing Haskell programs and web systems from a foundational and practical angle.
Now at UCSD
I co-supervised Filippo on information erasure and preserving privacy on systems subjected to transient faults.
Now at Admeta AB
I supervised Dante on security models for reactive systems. Dante took a full time position at FCEIA, UNR, Argentina and paused his studies.
Now at FCEIA, UNR
I supervised Juanjo when building a taint analysis for Python as a library.
Now at Avature
I supervised Albert on combining different notions of integrity for a security library in Haskell.
I co-supervised Ta-Chung on designing and implementing a security library in Haskell based on arrows.
(PI) This project develops techniques to combine static and dynamic analysis for information-flow control so that (i) developers must control the boundaries of static and dynamic analyses, (ii) enforcement techniques should be easily deployed in ubiquitous hardware and software, and (iii) the proposed solutions must be provably sound. The project also explores the use of the forthcoming Intel support for security, called Software Guard Extension, to safely deploy IFC techniques in cloud services.
Duration: 4 years (2016 - 2020)
Duration: 4 years (2015 - 2019)
(PI) This projects develops foundations to understands systems which release sensitive information using capability-like declassification mechanisms. The funds support a collaboration with Prof. Stephen Chong and his group at Harvard University.
Duration: 1 years (2014)
(PI) This project developed several solutions to remove information leaks in information-flow control systems due to timing perturbations arising from hardware, e.g., caches, TLB, etc. The funds supported a collaboration with Prof. David Mazières and his group at Stanford University.
Duration: 1 years (2013)
(PI) This project focus on developing technology to track how sensitive information flows within concurrent systems. We provide solutions for dynamically enforce confidentiality in Haskell.
Duration: 4 years (2012 - 2016)