System-level non-interference of constant-time cryptography. I: Model

DOI10.1007/s10817-017-9441-5zbMath1459.68026OpenAlexW2772681170MaRDI QIDQ2417947

Carlos Luna, Gustavo Betarte, Juan Diego Campo, Gilles Barthe

Publication date: 31 May 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9441-5

Mathematics Subject Classification ID

Cryptography (94A60) Computer security (68M25)

Related Items (3)

Timed hyperproperties ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ Automated proof of Bell-LaPadula security properties

Uses Software

• ACL2
• Coq
• VCC
• seL4
• Rocksalt

Cites Work

• Unnamed Item
• Unnamed Item
• Certifying low-level programs with hardware interrupts and preemptive threads
• Formal memory models for the verification of low-level operating-system code
• Operating system verification---an overview
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• Efficient cache attacks on AES, and countermeasures
• Deep Specifications and Certified Abstraction Layers
• Parametric Verification of Address Space Separation
• Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
• Formally Verified Implementation of an Idealized Model of Virtualization
• seL4 Enforces Integrity
• Faster and Timing-Attack Resistant AES-GCM
• A fast new DES implementation in software
• Modular verification of preemptive OS kernels
• Formal certification of a compiler back-end or
• A Vulnerability in RSA Implementations Due to Instruction Cache Analysis and Its Demonstration on OpenSSL
• Topics in Cryptology – CT-RSA 2006
• Theory of Cryptography

This page was built for publication: System-level non-interference of constant-time cryptography. I: Model