Zobrazeno 1 - 10
of 158
pro vyhledávání: '"Jhala, Ranjit"'
Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof en
Externí odkaz:
http://arxiv.org/abs/2405.16792
Autor:
Kolosick, Matthew, Shivakumar, Basavesh Ammanaghatta, Cauligi, Sunjay, Patrignani, Marco, Vassena, Marco, Jhala, Ranjit, Stefan, Deian
The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory accesses, and thus avoids leaking secrets through cache and timing si
Externí odkaz:
http://arxiv.org/abs/2311.05831
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-t
Externí odkaz:
http://arxiv.org/abs/2207.05617
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rus
Externí odkaz:
http://arxiv.org/abs/2207.04034
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 higher-order specifications. Ghost variables circumvent this limitati
Externí odkaz:
http://arxiv.org/abs/2105.01954
Autor:
Kolosick, Matthew, Narayan, Shravan, Johnson, Evan, Watt, Conrad, LeMay, Michael, Garg, Deepak, Jhala, Ranjit, Stefan, Deian
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and compan
Externí odkaz:
http://arxiv.org/abs/2105.00033
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 the effort needed to localize the root cause of verification failures v
Externí odkaz:
http://arxiv.org/abs/2104.00461
Autor:
Jhala, Ranjit, Vazou, Niki
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 knob with which to inform the type system about what invariants and co
Externí odkaz:
http://arxiv.org/abs/2010.07763
Autor:
Vassena, Marco, Disselkoen, Craig, Gleissenthall, Klaus V., Cauligi, Sunjay, Kici, Rami Gökhan, Jhala, Ranjit, Tullsen, Dean, Stefan, Deian
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 speculation, it suffices to $\textit{cut}$ the dataflow from expressions tha
Externí odkaz:
http://arxiv.org/abs/2005.00294