A formal verification of mutation-based moving target defense

Muhammad Abdul Basit Ur Rahim; Qi Duan; Ehab Al-Shaer

doi:10.1145/3314058.3317723

A formal verification of mutation-based moving target defense

Muhammad Abdul Basit Ur Rahim
, Qi Duan
, Ehab Al-Shaer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Static system configuration provides the advantage for the attackers to discover the vulnerabilities of the system and launch attacks. Moving Target Defense (MTD) can break this asymmetry for the defenders by mutating certain configuration parameters proactively and at the same time maintaining the run-time correctness and operational integrity. MTD is essentially distributed by nature since the processes or actions in MTD are executed in an interleaved manner. For any distributed system, it is important to verify the correctness and integrity, since they may be jeopardized by design errors or run time inconsistencies. In this work we present a framework for formal verification of MTD techniques. We describe MTD techniques with formal ontology and model the system behaviors with timed automata, and verify the correctness, liveness, fairness and deadlock-free properties of the system. We use Random Host Mutation (RHM) as the case study or MTD formal verification. Our experimentation validates the feasibility and scalability of the formal verification framework.

Original language	English
Title of host publication	Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019
Publisher	Association for Computing Machinery
ISBN (Electronic)	9781450371476
DOIs	https://doi.org/10.1145/3314058.3317723
State	Published - 1 Apr 2019
Externally published	Yes
Event	6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019 - Nashville, United States Duration: 1 Apr 2019 → 3 Apr 2019

Publication series

Name	ACM International Conference Proceeding Series

Conference

Conference	6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019
Country/Territory	United States
City	Nashville
Period	1/04/19 → 3/04/19

Bibliographical note

Publisher Copyright:
© 2019 Copyright held by the owner/author(s).

ASJC Scopus subject areas

Software
Human-Computer Interaction
Computer Vision and Pattern Recognition
Computer Networks and Communications

Access to Document

10.1145/3314058.3317723

Cite this

@inproceedings{468c50d282d9420db48612f92dd12d98,

title = "A formal verification of mutation-based moving target defense",

abstract = "Static system configuration provides the advantage for the attackers to discover the vulnerabilities of the system and launch attacks. Moving Target Defense (MTD) can break this asymmetry for the defenders by mutating certain configuration parameters proactively and at the same time maintaining the run-time correctness and operational integrity. MTD is essentially distributed by nature since the processes or actions in MTD are executed in an interleaved manner. For any distributed system, it is important to verify the correctness and integrity, since they may be jeopardized by design errors or run time inconsistencies. In this work we present a framework for formal verification of MTD techniques. We describe MTD techniques with formal ontology and model the system behaviors with timed automata, and verify the correctness, liveness, fairness and deadlock-free properties of the system. We use Random Host Mutation (RHM) as the case study or MTD formal verification. Our experimentation validates the feasibility and scalability of the formal verification framework.",

author = "Rahim, \{Muhammad Abdul Basit Ur\} and Qi Duan and Ehab Al-Shaer",

note = "Publisher Copyright: {\textcopyright} 2019 Copyright held by the owner/author(s).; 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019 ; Conference date: 01-04-2019 Through 03-04-2019",

year = "2019",

month = apr,

day = "1",

doi = "10.1145/3314058.3317723",

language = "English",

series = "ACM International Conference Proceeding Series",

publisher = "Association for Computing Machinery",

booktitle = "Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019",

}

Rahim, MABU, Duan, Q & Al-Shaer, E 2019, A formal verification of mutation-based moving target defense. in Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019., a10, ACM International Conference Proceeding Series, Association for Computing Machinery, 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019, Nashville, United States, 1/04/19. https://doi.org/10.1145/3314058.3317723

A formal verification of mutation-based moving target defense. / Rahim, Muhammad Abdul Basit Ur; Duan, Qi; Al-Shaer, Ehab.
Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019. Association for Computing Machinery, 2019. a10 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A formal verification of mutation-based moving target defense

AU - Rahim, Muhammad Abdul Basit Ur

AU - Duan, Qi

AU - Al-Shaer, Ehab

PY - 2019/4/1

Y1 - 2019/4/1

N2 - Static system configuration provides the advantage for the attackers to discover the vulnerabilities of the system and launch attacks. Moving Target Defense (MTD) can break this asymmetry for the defenders by mutating certain configuration parameters proactively and at the same time maintaining the run-time correctness and operational integrity. MTD is essentially distributed by nature since the processes or actions in MTD are executed in an interleaved manner. For any distributed system, it is important to verify the correctness and integrity, since they may be jeopardized by design errors or run time inconsistencies. In this work we present a framework for formal verification of MTD techniques. We describe MTD techniques with formal ontology and model the system behaviors with timed automata, and verify the correctness, liveness, fairness and deadlock-free properties of the system. We use Random Host Mutation (RHM) as the case study or MTD formal verification. Our experimentation validates the feasibility and scalability of the formal verification framework.

AB - Static system configuration provides the advantage for the attackers to discover the vulnerabilities of the system and launch attacks. Moving Target Defense (MTD) can break this asymmetry for the defenders by mutating certain configuration parameters proactively and at the same time maintaining the run-time correctness and operational integrity. MTD is essentially distributed by nature since the processes or actions in MTD are executed in an interleaved manner. For any distributed system, it is important to verify the correctness and integrity, since they may be jeopardized by design errors or run time inconsistencies. In this work we present a framework for formal verification of MTD techniques. We describe MTD techniques with formal ontology and model the system behaviors with timed automata, and verify the correctness, liveness, fairness and deadlock-free properties of the system. We use Random Host Mutation (RHM) as the case study or MTD formal verification. Our experimentation validates the feasibility and scalability of the formal verification framework.

UR - https://www.scopus.com/pages/publications/85068776530

U2 - 10.1145/3314058.3317723

DO - 10.1145/3314058.3317723

M3 - Conference contribution

AN - SCOPUS:85068776530

T3 - ACM International Conference Proceeding Series

BT - Proceedings of the 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019

PB - Association for Computing Machinery

T2 - 6th Annual Symposium on Hot Topics in the Science of Security, HotSoS 2019

Y2 - 1 April 2019 through 3 April 2019

ER -

A formal verification of mutation-based moving target defense

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this