{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:12:48Z","timestamp":1762863168451,"version":"3.41.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR national research program PACS","award":["ANR-14-CE28-0002"],"award-info":[{"award-number":["ANR-14-CE28-0002"]}]},{"name":"ANR-NRF research program ProMiS","award":["ANR-19-CE25-0015"],"award-info":[{"award-number":["ANR-19-CE25-0015"]}]},{"name":"ERATO HASUO Metamathematics for Systems Design Project","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3502851","type":"journal-article","created":{"date-parts":[[2022,7,9]],"date-time":"2022-07-09T13:17:39Z","timestamp":1657372659000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Guaranteeing Timed Opacity using Parametric Timed Model Checking"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9429-7586","authenticated-orcid":false,"given":"Didier","family":"Lime","sequence":"additional","affiliation":[{"name":"\u00c9cole Centrale de Nantes, LS2N, UMR CNRS 6004, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2548-6196","authenticated-orcid":false,"given":"Dylan","family":"Marinho","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, Inria, LORIA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"School of Information Systems, Singapore Management University, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,8]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-008-0058-x"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167242"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_7"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/309831.309888"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/352600.352606"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242656"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516712"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1080\/00207179.2014.944356"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.046"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/2371116.2371118"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/2370741.2370744"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS51672.2020.00012"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02617-1_3"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00173-4"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2021.102926"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63121-9_1"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_2"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94496-8_3"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01461-2_3"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2857363"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1342991.1342996"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29662-9_11"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(1:7)2007"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-021-00606-2"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3399742"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325702"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.19"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3090064.3090071"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213851"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.031"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240485"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.25"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-53946-1_5"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_12"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66595-5_3"},{"key":"e_1_3_3_42_2","first-page":"431","volume-title":"Proceedings of the USENIX Security Symposium","author":"Doychev Goran","year":"2013","unstructured":"Goran Doychev, Dominik Feld, Boris K\u00f6pf, Laurent Mauborgne, and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In Proceedings of the USENIX Security Symposium. 431\u2013446."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236028"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461358"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99629"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2357445"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006905"},{"key":"e_1_3_3_49_2","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","year":"1999","unstructured":"Alexander Schrijver. 1999. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_26"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0467-0"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_26"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2006.11.018"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_6"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0074-0"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2017.19"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00151-3_3"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:5)2020"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_12"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2010.30"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2021.36"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3502851","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3502851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:34Z","timestamp":1750188634000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3502851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,8]]},"references-count":65,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3502851"],"URL":"https:\/\/doi.org\/10.1145\/3502851","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2022,9,8]]},"assertion":[{"value":"2020-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}