Guaranteeing Timed Opacity using Parametric Timed Model Checking
| Autor: | Étienne André, Dylan Marinho, Jun Sun, Didier Lime |
|---|---|
| Přispěvatelé: | Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-École Centrale de Nantes (Nantes Univ - ECN), Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST), Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie, Nantes Université (Nantes Univ), School of Information Systems (Singapore Management University - SMU) (SIS - SMU), This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), by the ANR-NRF research program ProMiS (ANR-19-CE25-0015), and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST., Agence Nationale de la Recherche (ANR), ANR-14-CE28-0002,PACS,Analyses paramétrées de systèmes concurrents(2014), ANR-19-CE25-0015,ProMiS,Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée(2019) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Computer Science - Cryptography and Security parameter synthesis Formal Languages and Automata Theory (cs.FL) opacity [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] parametric timed automata Computer Science - Formal Languages and Automata Theory Logic in Computer Science (cs.LO) [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] timed automata IMITATOR Cryptography and Security (cs.CR) Software |
| Zdroj: | ACM Transactions on Software Engineering and Methodology ACM Transactions on Software Engineering and Methodology, 2022, 31 (4), pp.1-36. ⟨10.1145/3502851⟩ |
| ISSN: | 1049-331X |
| Popis: | Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully deduces confidential internal information. In this work, we consider that the attacker has access (only) to the system execution time. We address the following timed opacity problem: given a timed system, a private location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the system went through the private location. We also consider the full timed opacity problem, asking whether the system is opaque for all execution times. We show that these problems are decidable for timed automata (TAs) but become undecidable when one adds parameters, yielding parametric timed automata (PTAs). We identify a subclass with some decidability results. We then devise an algorithm for synthesizing PTAs parameter valuations guaranteeing that the resulting TA is opaque. We finally show that our method can also apply to program analysis. This is the author version of the manuscript of the same name published in ACM Transactions on Software Engineering and Methodology (ToSEM). This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), by the ANR-NRF research program ProMiS (ANR-19-CE25-0015), and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. arXiv admin note: substantial text overlap with arXiv:1907.00537 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|