Projects

Active projects

  • Cryptography: Cryptosense is a spin-off co-founded by Riccardo Focardi that produces software for security analysis of cryptographic systems, in particular in banks and other security-sensitive environments. Cryptosense started after the Tookan project demonstrated the potential of the technological transfer of formal verification techniques into the field of IT security. In a recent paper presented at NDSS’18 (video) we have found critical vulnerabilities in Java Keystores that lead to three CVEs from Oracle:
  • Network Security: Mignis is a semantic-based tool for firewall configuration. It allows for simple declarative firewall specifications that are compiled into real Netfilter (iptables) rules. A theorem guarantees that the translation preserves the semantics. Mignis has been presented at IEEE CSF’14 and is available on github. Our recent results on firewall analysis have been presented at international venues, among which Euro S&P 2018.
  • Web Security: NEW our paper on TLS security analysis in the wild has been presented at IEEE S&P 2019 and covered on wired! See the preview video and the dedicated web page for more detail.
    Previous work on web security regarded the development of security extensions of the Chrome browser that implement client-side mechanisms to improve web security (ESSOS’14 and IEEE CSF’14).
  • Embedded Systems Security: NEW Voltage fault injection is a powerful active side channel attack that modifies the execution-flow of a device by creating disturbances on the power supply line. We have proposed a new voltage fault injection technique that generates fully arbitrary voltage glitch waveforms using off-the-shelf and low cost equipment. To show the effectiveness of our setup, we have presented new, unpublished firmware extraction attacks on six microcontrollers from three major manufacturers: STMicroelectronics, Texas Instruments and Renesas Electronics. Results have been published in IACR TCHES 2019.
    Previous research on APDU-level attacks on crypto tokens has been published at RAID 2016. Here you can find more detail.

Old projects

  • Gran is tool for the analysis of RBAC grsecurity policies based on a formal semantics. It has been presented at IEEE CSF’12 and is available on github.
  • Tookan is an automated tool which reverse-engineers a real PKCS#11 token to deduce its functionality, constructs a model of its API for the SATMC model checker, and then executes any attack trace found by the model checker directly on the token.
  • Cryptokix is software token with security fixes, based on openCryptoki. Its security is highly configurable by selectively enabling different patches.
  • Kerberos Login Service. We implemented and discussed fixes for the “pass-the-ticket” attack on various Microsoft Windows Kerberos implementations. See the paper for more detail.