16 citations · 19 across the 7 of their papers we have counts for
12 papers
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express…
Solver-Aided Constant-Time Circuit Verification
Rami Gokhan Kici, Klaus v. Gleissenthall, Deian Stefan +1
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing t…
Refinement Types: A Tutorial
Ranjit Jhala, Niki Vazou
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable…
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall +5
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via specul…
Iodine: Verifying Constant-Time Execution of Hardware
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan +1
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing ch…
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri +2
Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate…