We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.CR

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Cryptography and Security

Title: Parametric Timed Model Checking for Guaranteeing Timed Opacity

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.
Comments: This is the author (and extended) version of the manuscript of the same name published in the proceedings of ATVA 2019. This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002), the ANR-NRF research program (ProMiS) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)
Journal reference: Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Springer LNCS 11781, pages 115-130, 2019
DOI: 10.1007/978-3-030-31784-3_7
Cite as: arXiv:1907.00537 [cs.CR]
  (or arXiv:1907.00537v2 [cs.CR] for this version)

Submission history

From: Étienne André [view email]
[v1] Mon, 1 Jul 2019 04:27:31 GMT (156kb)
[v2] Tue, 29 Oct 2019 06:46:50 GMT (182kb,D)

Link back to: arXiv, form interface, contact.