Parametric Timed Model Checking for Guaranteeing Timed Opacity

DOI10.1007/978-3-030-31784-3_7MaRDI QIDQ3297588zbMATH OpenOpenAlexFDO

Authors Étienne André, Jun Sun

Publication date 20 July 2020

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1907.00537, https://ink.library.smu.edu.sg/sis_research/4966

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis.

Recommendations

• Bounded Model Checking for Parametric Timed Automata
• Parameterised model checking for alternating-time temporal logic
• Durations and parametric model-checking in timed automata
• Formal Modeling and Analysis of Timed Systems
• Towards integrated verification of timed transition models
• Model-checking timed temporal logics
• scientific article; zbMATH DE number 1973987
• Validation of Stochastic Systems
• Formal Techniques for Networked and Distributed Systems - FORTE 2005

Cites work

• \textsc{SCInfer}: refinement-based verification of software countermeasures against side-channel attacks
• A theory of timed automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Control and synthesis of non-interferent timed systems
• scientific article; zbMATH DE number 1799514 (Why is no real title available?)
• Information flow for timed automata
• Linear parametric model checking of timed automata
• Non-interference control synthesis for security timed automata
• Parametric real-time reasoning
• Secure information release in timed automata
• Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems

Cited in

(5)

• Secure information release in timed automata
• Transforming out timing leaks
• Automated Technology for Verification and Analysis
• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
• Tempus fugit: How to plug it

Describes a project that uses

Uses Software

• CacheAudit
• IMITATOR

This page was built for publication: Parametric Timed Model Checking for Guaranteeing Timed Opacity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297588)