Privacy-preserving co-synthesis against sensor-actuator eavesdropping intruder?

被引:2
作者
Tai, Ruochen [1 ]
Lin, Liyong [1 ]
Zhu, Yuting [1 ]
Su, Rong [1 ]
机构
[1] Nanyang Technol Univ, Sch Elect & Elect Engn, 50 Nanyang Ave, Singapore 639798, Singapore
关键词
Privacy-preserving; Supervisory control; Opacity enforcement; Dynamic mask; Edit function; Supervisor; ENFORCING SUPERVISORY STRATEGIES; OPACITY; ENFORCEMENT; SYSTEMS; SECURE; NOTIONS;
D O I
10.1016/j.automatica.2023.110860
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
In this work, we investigate the problem of privacy-preserving supervisory control against an external passive intruder via co-synthesis of a dynamic mask, an edit function, and a supervisor. We attempt to achieve the following goals: (1) the system secret cannot be inferred by the intruder, i.e., opacity of secrets against the intruder, and the existence of the dynamic mask and the edit function should not be discovered by the intruder, i.e., covertness of dynamic mask and edit function against the intruder; (2) some safety and nonblockingness requirement should be satisfied. We assume the intruder can eavesdrop both the sensing information generated by the sensors and the control commands issued to the actuators. Our approach is to model the co-synthesis problem as a distributed supervisor synthesis problem in the Ramadge-Wonham supervisory control framework, and we propose an incremental synthesis heuristic to incrementally synthesize a dynamic mask, an edit function and a supervisor. The effectiveness of our approach is illustrated on an example about location privacy. (c) 2023 Elsevier Ltd. All rights reserved.
引用
收藏
页数:13
相关论文
共 46 条
  • [1] Akesson K, 2006, WODES 2006: EIGHTH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, PROCEEDINGS, P384
  • [2] Alexandru AB, 2018, IEEE DECIS CONTR P, P5014, DOI 10.1109/CDC.2018.8619835
  • [3] Enforcing current-state opacity through shuffle in event observations
    Barcelos, Raphael Julio
    Basilio, Joao Carlos
    [J]. IFAC PAPERSONLINE, 2018, 51 (07): : 100 - 105
  • [4] Quantifying opacity
    Berard, Beatrice
    Mullins, John
    Sassolas, Mathieu
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2015, 25 (02) : 361 - 403
  • [5] Biere A, 2003, ADV COMPUT, V58, P117
  • [6] Bounded model checking
    Biere, Armin
    [J]. Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 457 - 481
  • [7] Synthesis of opaque systems with static and dynamic masks
    Cassez, Franck
    Dubreil, Jeremy
    Marchand, Herve
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) : 88 - 115
  • [8] Enforcing opacity of regular predicates on modal transition systems
    Darondeau, Philippe
    Marchand, Herve
    Ricker, Laurie
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2015, 25 (1-2): : 251 - 270
  • [9] Encrypted Control for Networked Systems AN ILLUSTRATIVE INTRODUCTION AND CURRENT CHALLENGES
    Darup, Moritz Schulze
    Alexandru, Andreea B.
    Quevedo, Daniel E.
    Pappas, George J.
    [J]. IEEE CONTROL SYSTEMS MAGAZINE, 2021, 41 (03): : 58 - 78
  • [10] Opacity enforcing control synthesis
    Dubreil, Jeremy
    Darondeau, Philippe
    Marchand, Herve
    [J]. WODES' 08: PROCEEDINGS OF THE 9TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, 2008, : 28 - 35