PRIYA , Swarn

Developers of high-assurance software aim to design functionally correct software with properties like confidentiality. However, confidentiality is not a direct consequence of functional correctness, as there could be unintentional side-channel leaks like execution time that might help the attacker to retrieve secret data.For example, a...

Developers of high-assurance software aim to design functionally correct software with properties like confidentiality. However, confidentiality is not a direct consequence of functional correctness, as there could be unintentional side-channel leaks like execution time that might help the attacker to retrieve secret data.For example, a...

Many security properties of interest are captured by instrumented semantics that model the functional behavior and the leakage of programs. For several important properties, including cryptographic constant-time (CCT), leakage models are sufficiently abstract that one can define instrumented semantics for high-level and low-level programs. One...

Cryptographic constant-time (CT) is a popular programming discipline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program execution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, sometimes even...

High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution...

The current gold standard of cryptographic software is to write efficient libraries with systematic protections against timing attacks. In order to meet this goal, cryptographic engineers increasingly use high-assurance cryptography tools. These tools guide programmers and provide rigorous guarantees that can be verified independently by...