Active projects

  • 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.
  • 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.
  • CookieExt and SessInt are extensions of the Chrome browser that implement client-side mechanisms to improve web security. Security has been formally proved on a model of the extensions presented at ESSOS’14 and IEEE CSF’14.
  • 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.

Old projects

  • 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.