Leader of the formal verification (FA2) research area of the VeriWeird project. VeriWeird’s key innovation is to develop a novel approach to the formalzation of hidden communication systems (HCS) that is based on the encoding of (HCS) properties in the simulation-based cryptgraphy proof paradigm.
Leader of the Computer-Aided Cryptography for Health (CAC-H) task, part of the Cognitive Health Assistant that Learns and Organizes (CHALO) project, part of the Digital Health Security (DIGIHEALS) ARPA-H program.
Co-Principal Investigator of the End-to-end Machinery for Proving Highly sensitive Application-oriented Statements In ZEro-knowledge (EMPHASIZE) project, part of the Securing Information for Encrypted Verification and Evaluation (SIEVE) DARPA program.
Principal Investigator of the Automated-instrumentation of Legacy Insecure Cryptographic Executables (ALICE) project.