Andrew Ferraiuolo

Currently, I am a researcher employed in the research and development department of Certora, where I work on formal verification of smart contracts.

Previously I was a Research Scientist at Google Research, where I developed privacy preserving technologies. My projects included: developing tools and theoretical foundations for formal verification of commercial hypervisors; designing and verifying an information flow control runtime with formal security guarantees; developing a declarative, logic-based privacy policy language; contributing to a dataflow analysis framework specialized for privacy use-cases; and collaborating on static analyses for differential privacy.

Before that, I was a Hardware Engineer at Google (on a different team), ensuring Google smartphones are resilient to physical attacks. In particular, I developed mitigations for power side channel attacks, performed side-channel penetration testing, and explored formal methods tools that could provide formal security guarantees such as T-Probing Security.

At Microsoft Research, I collaborated on Komodo a formally verified Trusted Execution Environment (also called an "enclave") with machine-checked proofs of correctness and comprehensive information flow security theorems.

As a PhD student at Cornell, I won the department's Best Dissertation Award for my research combining programming languages and computer architecture techniques to prevent timing channel attacks. This work began 5 years before Spectre/Meltdown drew significant attention to this problem. My research entailed both novel computer archtiectures to mitigate these attacks, and programming language tools that ensure hardware designs are not vulnerable to timing channels. In particular I developed novel microarchitectures for caches, microcontrollers, and full processors that coordinate scheduling to achieve high performance while still preventing these attacks. I also developed a hardware description language equipped with an information flow type system that efficiently proves the hardware has a timing-sensitive variant of noninterference. It supports dependant types that can express functional correctness conditions that are dispatched to an SMT solver.

As an undergraduate researcher at the University of Connecticut, I worked on novel techniques for detecting hardware trojan attacks which are attacks on computer hardware supply chains, for example, when nation-state actors compromise a hardware fabrication facility. As a result of this work, I published 3 papers, and won the department's best senior design project award.