PLSec-VU on GitHub
Check out the group's GitHub repositories, tools, and artifacts.
Projects
Research directions, funded work, prototypes, and collaborations.
Haystack
Interactive explanations for refinement type checking failures.
Haystack studies how type checkers can produce useful counterexamples when verification fails. The project combines programming language theory with practical interfaces for debugging.
Pantomime
Constructive leakage proofs for hardware designs via simulation.
Pantomime is a tool for writing processors and their leakage proofs in Haskell. It supports simulation-based leakage proofs, where a simulator acts as an executable proof object showing that a leakage description captures the attacker-observable behavior of a hardware design.