A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems
In this paper, we present our results on the formal reliability analysis of the behavioral correctness of our cognitive middleware ARMET. The formally assured behavioral correctness of a software system is a fundamental prerequisite for the system’s security. Therefore, the goal of this study is to,...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Published: |
MDPI AG
2018
|
| Online Access: | http://hdl.handle.net/1721.1/113337 |
| _version_ | 1826205901944520704 |
|---|---|
| author | Khan, Muhammad Taimoor Serpanos, Dimitrios Khan, Muhammad Shrobe, Howard E |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Khan, Muhammad Taimoor Serpanos, Dimitrios Khan, Muhammad Shrobe, Howard E |
| author_sort | Khan, Muhammad Taimoor |
| collection | MIT |
| description | In this paper, we present our results on the formal reliability analysis of the behavioral correctness of our cognitive middleware ARMET. The formally assured behavioral correctness of a software system is a fundamental prerequisite for the system’s security. Therefore, the goal of this study is to, first, formalize the behavioral semantics of the middleware and, second, to prove its behavioral correctness. In this study, we focus only on the core and critical component of the middleware: the execution monitor. The execution monitor identifies inconsistencies between runtime observations of an industrial control system (ICS) application and predictions of the specification of the application. As a starting point, we have defined the formal (denotational) semantics of the observations (produced by the application at run-time), and predictions (produced by the executable specification of the application). Then, based on the formal semantices, we have formalized the behavior of the execution monitor. Finally, based on the semantics, we have proved soundness (absence of false alarms) and completeness (detection of arbitrary attacks) to assure the behavioral correctness of the monitor. Keywords: run-time monitoring; security monitor; absence of false alarms; ICS; CPS |
| first_indexed | 2024-09-23T13:20:51Z |
| format | Article |
| id | mit-1721.1/113337 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T13:20:51Z |
| publishDate | 2018 |
| publisher | MDPI AG |
| record_format | dspace |
| spelling | mit-1721.1/1133372022-10-01T14:42:43Z A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems Khan, Muhammad Taimoor Serpanos, Dimitrios Khan, Muhammad Shrobe, Howard E Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Shrobe, Howard E In this paper, we present our results on the formal reliability analysis of the behavioral correctness of our cognitive middleware ARMET. The formally assured behavioral correctness of a software system is a fundamental prerequisite for the system’s security. Therefore, the goal of this study is to, first, formalize the behavioral semantics of the middleware and, second, to prove its behavioral correctness. In this study, we focus only on the core and critical component of the middleware: the execution monitor. The execution monitor identifies inconsistencies between runtime observations of an industrial control system (ICS) application and predictions of the specification of the application. As a starting point, we have defined the formal (denotational) semantics of the observations (produced by the application at run-time), and predictions (produced by the executable specification of the application). Then, based on the formal semantices, we have formalized the behavior of the execution monitor. Finally, based on the semantics, we have proved soundness (absence of false alarms) and completeness (detection of arbitrary attacks) to assure the behavioral correctness of the monitor. Keywords: run-time monitoring; security monitor; absence of false alarms; ICS; CPS 2018-01-29T19:49:21Z 2018-01-29T19:49:21Z 2017-08 2017-05 2018-01-24T21:04:41Z Article http://purl.org/eprint/type/JournalArticle 2079-9292 http://hdl.handle.net/1721.1/113337 Khan, Muhammad et al. "A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems." Electronics 6, 3 (August 2017): 58 © 2017 The Author(s) http://dx.doi.org/10.3390/electronics6030058 Electronics Creative Commons Attribution http://creativecommons.org/licenses/by/4.0/ application/pdf MDPI AG Multidisciplinary Digital Publishing Institute |
| spellingShingle | Khan, Muhammad Taimoor Serpanos, Dimitrios Khan, Muhammad Shrobe, Howard E A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title | A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title_full | A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title_fullStr | A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title_full_unstemmed | A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title_short | A Formally Reliable Cognitive Middleware for the Security of Industrial Control Systems |
| title_sort | formally reliable cognitive middleware for the security of industrial control systems |
| url | http://hdl.handle.net/1721.1/113337 |
| work_keys_str_mv | AT khanmuhammadtaimoor aformallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT serpanosdimitrios aformallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT khanmuhammad aformallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT shrobehowarde aformallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT khanmuhammadtaimoor formallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT serpanosdimitrios formallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT khanmuhammad formallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems AT shrobehowarde formallyreliablecognitivemiddlewareforthesecurityofindustrialcontrolsystems |