Enforcing opacity by insertion functions under multiple energy constraints

被引:44
作者
Ji, Yiding [1 ]
Yin, Xiang [2 ]
Lafortune, Stephane [1 ]
机构
[1] Univ Michigan, Dept Elect Engn & Comp Sci, Ann Arbor, MI 48109 USA
[2] Shanghai Jiao Tong Univ, Dept Automat, Shanghai, Peoples R China
基金
美国国家科学基金会; 中国国家自然科学基金;
关键词
Discrete event systems; Opacity enforcement; Insertion function; Partial observation; Quantitative games; DISCRETE-EVENT SYSTEMS; K-STEP OPACITY; INFINITE-STEP; ENFORCEMENT; VERIFICATION; NOTIONS;
D O I
10.1016/j.automatica.2019.06.028
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
This paper investigates the enforcement of opacity by insertion functions subject to multiple quantitative constraints capturing resource or energy limitations. There is a malicious intruder attempting to infer secrets of the system from its observations. To prevent the disclosure of secrets, the insertion function inserts fictitious events to the output of the system to obfuscate the intruder. The system is initialized with several types of resources, referred to as energy. The energy is consumed or replenished with event occurrences while always consumed with event insertions. The insertion function must enforce opacity while ensuring that each type of resource is never depleted. This problem is then reduced to a two-player game between the insertion function and the system (environment), with properly defined objectives. A game structure called the Energy Insertion Structure, denoted by EIS is proposed, which provably contains solutions to the energy constrained opacity enforcement problem. Then we further study the bounded cost rate insertion problem on the insertion function's winning region of EIS, which requires that the long run average rate of insertion cost be bounded. This problem is formulated as a multidimensional mean payoff game and a special method called hyperplane separation technique is applied to efficiently solve it. (C) 2019 Elsevier Ltd. All rights reserved.
引用
收藏
页数:14
相关论文
共 40 条
[1]  
[Anonymous], 2011, LECT GAME THEORY COM
[2]   Enforcing current-state opacity through shuffle in event observations [J].
Barcelos, Raphael Julio ;
Basilio, Joao Carlos .
IFAC PAPERSONLINE, 2018, 51 (07) :100-105
[3]   Quantifying opacity [J].
Berard, Beatrice ;
Mullins, John ;
Sassolas, Mathieu .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2015, 25 (02) :361-403
[4]  
Boyd Stephen P., 2014, Convex Optimization
[5]   Faster algorithms for mean-payoff games [J].
Brim, L. ;
Chaloupka, J. ;
Doyen, L. ;
Gentilini, R. ;
Raskin, J. F. .
FORMAL METHODS IN SYSTEM DESIGN, 2011, 38 (02) :97-118
[6]  
Cassandras C. G., 2007, INTRO DISCRETE EVENT, V2nd
[7]   Synthesis of opaque systems with static and dynamic masks [J].
Cassez, Franck ;
Dubreil, Jeremy ;
Marchand, Herve .
FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) :88-115
[8]  
Cassez F, 2009, LECT NOTES COMPUT SC, V5576, P21, DOI 10.1007/978-3-642-02617-1_3
[9]   Hyperplane separation technique for multidimensional mean-payoff games [J].
Chatterjee, Krishnendu ;
Velner, Yaron .
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2017, 88 :236-259
[10]   Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems [J].
Chedor, Sebastien ;
Morvan, Christophe ;
Pinchinat, Sophie ;
Marchand, Herve .
DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2015, 25 (1-2) :271-294