Parametric timed model checking for guaranteeing timed opacity
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, synthe...
Saved in:
Main Authors: | , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2019
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4966 https://ink.library.smu.edu.sg/context/sis_research/article/5969/viewcontent/André_Sun2019_Chapter_ParametricTimedModelCheckingFo.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5969 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59692020-03-12T07:23:57Z Parametric timed model checking for guaranteeing timed opacity ANDRÉ, Étienne SUN, Jun 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. 2019-10-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4966 info:doi/10.1007/978-3-030-31784-3_7 https://ink.library.smu.edu.sg/context/sis_research/article/5969/viewcontent/André_Sun2019_Chapter_ParametricTimedModelCheckingFo.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Opacity Timed automata IMITATOR Parameter synthesis Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Opacity Timed automata IMITATOR Parameter synthesis Software Engineering |
spellingShingle |
Opacity Timed automata IMITATOR Parameter synthesis Software Engineering ANDRÉ, Étienne SUN, Jun Parametric timed model checking for guaranteeing timed opacity |
description |
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. |
format |
text |
author |
ANDRÉ, Étienne SUN, Jun |
author_facet |
ANDRÉ, Étienne SUN, Jun |
author_sort |
ANDRÉ, Étienne |
title |
Parametric timed model checking for guaranteeing timed opacity |
title_short |
Parametric timed model checking for guaranteeing timed opacity |
title_full |
Parametric timed model checking for guaranteeing timed opacity |
title_fullStr |
Parametric timed model checking for guaranteeing timed opacity |
title_full_unstemmed |
Parametric timed model checking for guaranteeing timed opacity |
title_sort |
parametric timed model checking for guaranteeing timed opacity |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2019 |
url |
https://ink.library.smu.edu.sg/sis_research/4966 https://ink.library.smu.edu.sg/context/sis_research/article/5969/viewcontent/André_Sun2019_Chapter_ParametricTimedModelCheckingFo.pdf |
_version_ |
1770575161635897344 |