Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies
With the development of network technology, security in path planning problems has attracted widespread attention. We consider a path planning problem in which a planner computes a finite path that satisfies a specification. We assume that the specification includes mandatory safety/co-safety specif...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2023-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10035993/ |
| _version_ | 1811167541885665280 |
|---|---|
| author | Koki Kanashima Toshimitsu Ushio |
| author_facet | Koki Kanashima Toshimitsu Ushio |
| author_sort | Koki Kanashima |
| collection | DOAJ |
| description | With the development of network technology, security in path planning problems has attracted widespread attention. We consider a path planning problem in which a planner computes a finite path that satisfies a specification. We assume that the specification includes mandatory safety/co-safety specifications. Moreover, we consider a security policy for this path. However, we assume that the information leaked to an intruder is not known beforehand. Then, we propose an enforcement mechanism referred to as a finite-horizon shield. This mechanism modifies the path computed by the planner as small as possible to satisfy the safety/co-safety specifications and security policy under the leaked information. We assume that the safety/co-safety specifications are described by LTL<inline-formula> <tex-math notation="LaTeX">${}_{f}$ </tex-math></inline-formula> formulas and the security policy by a hyperLTL<inline-formula> <tex-math notation="LaTeX">${}_{f}$ </tex-math></inline-formula> formula. Subsequently, we convert the formulas into quantified formulas and compute the modified path using a satisfiability modulo theories solver. As an example, we consider an opacity problem where there is another path whose leaked information is the same as that of the modified path. By simulations, it confirms that the output of shield depends on the leaked information and the modified path may have additional movements to ensure opacity. We also compare the computation time of the shield with that of a security-aware planning by simulation. |
| first_indexed | 2024-04-10T16:12:10Z |
| format | Article |
| id | doaj.art-fd52f89c0de64da080c0debba64ca721 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-04-10T16:12:10Z |
| publishDate | 2023-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-fd52f89c0de64da080c0debba64ca7212023-02-10T00:00:36ZengIEEEIEEE Access2169-35362023-01-0111117661178010.1109/ACCESS.2023.324194610035993Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security PoliciesKoki Kanashima0https://orcid.org/0000-0001-5297-645XToshimitsu Ushio1https://orcid.org/0000-0002-4009-270XGraduate School of Engineering Science, Osaka University, Toyonaka, JapanGraduate School of Engineering Science, Osaka University, Toyonaka, JapanWith the development of network technology, security in path planning problems has attracted widespread attention. We consider a path planning problem in which a planner computes a finite path that satisfies a specification. We assume that the specification includes mandatory safety/co-safety specifications. Moreover, we consider a security policy for this path. However, we assume that the information leaked to an intruder is not known beforehand. Then, we propose an enforcement mechanism referred to as a finite-horizon shield. This mechanism modifies the path computed by the planner as small as possible to satisfy the safety/co-safety specifications and security policy under the leaked information. We assume that the safety/co-safety specifications are described by LTL<inline-formula> <tex-math notation="LaTeX">${}_{f}$ </tex-math></inline-formula> formulas and the security policy by a hyperLTL<inline-formula> <tex-math notation="LaTeX">${}_{f}$ </tex-math></inline-formula> formula. Subsequently, we convert the formulas into quantified formulas and compute the modified path using a satisfiability modulo theories solver. As an example, we consider an opacity problem where there is another path whose leaked information is the same as that of the modified path. By simulations, it confirms that the output of shield depends on the leaked information and the modified path may have additional movements to ensure opacity. We also compare the computation time of the shield with that of a security-aware planning by simulation.https://ieeexplore.ieee.org/document/10035993/HyperLTLopacitypath planningsafety/co-safety specificationsecurity policyshield synthesis |
| spellingShingle | Koki Kanashima Toshimitsu Ushio Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies IEEE Access HyperLTL opacity path planning safety/co-safety specification security policy shield synthesis |
| title | Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies |
| title_full | Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies |
| title_fullStr | Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies |
| title_full_unstemmed | Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies |
| title_short | Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies |
| title_sort | finite horizon shield for path planning ensuring safety co safety specifications and security policies |
| topic | HyperLTL opacity path planning safety/co-safety specification security policy shield synthesis |
| url | https://ieeexplore.ieee.org/document/10035993/ |
| work_keys_str_mv | AT kokikanashima finitehorizonshieldforpathplanningensuringsafetycosafetyspecificationsandsecuritypolicies AT toshimitsuushio finitehorizonshieldforpathplanningensuringsafetycosafetyspecificationsandsecuritypolicies |