A Formal Analysis of Moving Target Defense

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

doi:10.1109/COMPSAC48688.2020.00050

A Formal Analysis of 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

2 Scopus citations

Abstract

Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.

Original language	English
Title of host publication	Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020
Editors	W. K. Chan, Bill Claycomb, Hiroki Takakura, Ji-Jiang Yang, Yuuichi Teranishi, Dave Towey, Sergio Segura, Hossain Shahriar, Sorel Reisman, Sheikh Iqbal Ahamed
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1802-1807
Number of pages	6
ISBN (Electronic)	9781728173030
DOIs	https://doi.org/10.1109/COMPSAC48688.2020.00050
State	Published - Jul 2020
Externally published	Yes
Event	44th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2020 - Virtual, Madrid, Spain Duration: 13 Jul 2020 → 17 Jul 2020

Publication series

Name	Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020

Conference

Conference	44th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2020
Country/Territory	Spain
City	Virtual, Madrid
Period	13/07/20 → 17/07/20

Bibliographical note

Publisher Copyright:
© 2020 IEEE.

Keywords

Formal specification
Moving target defense
configuration-based mutation
model checking
verification

ASJC Scopus subject areas

Artificial Intelligence
Computer Networks and Communications
Computer Science Applications
Hardware and Architecture
Software
Education

Access to Document

10.1109/COMPSAC48688.2020.00050

Cite this

Abdul Basit Ur Rahim, M., Duan, Q., & Al-Shaer, E. (2020). A Formal Analysis of Moving Target Defense. In W. K. Chan, B. Claycomb, H. Takakura, J.-J. Yang, Y. Teranishi, D. Towey, S. Segura, H. Shahriar, S. Reisman, & S. I. Ahamed (Eds.), Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020 (pp. 1802-1807). Article 9202451 (Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/COMPSAC48688.2020.00050

Abdul Basit Ur Rahim, Muhammad ; Duan, Qi ; Al-Shaer, Ehab. / A Formal Analysis of Moving Target Defense. Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020. editor / W. K. Chan ; Bill Claycomb ; Hiroki Takakura ; Ji-Jiang Yang ; Yuuichi Teranishi ; Dave Towey ; Sergio Segura ; Hossain Shahriar ; Sorel Reisman ; Sheikh Iqbal Ahamed. Institute of Electrical and Electronics Engineers Inc., 2020. pp. 1802-1807 (Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020).

@inproceedings{24f276ae7b1c4140bc006ae1c6bd4450,

title = "A Formal Analysis of Moving Target Defense",

abstract = "Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.",

keywords = "Formal specification, Moving target defense, configuration-based mutation, model checking, verification",

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

note = "Publisher Copyright: {\textcopyright} 2020 IEEE.; 44th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2020 ; Conference date: 13-07-2020 Through 17-07-2020",

year = "2020",

month = jul,

doi = "10.1109/COMPSAC48688.2020.00050",

language = "English",

series = "Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "1802--1807",

editor = "Chan, \{W. K.\} and Bill Claycomb and Hiroki Takakura and Ji-Jiang Yang and Yuuichi Teranishi and Dave Towey and Sergio Segura and Hossain Shahriar and Sorel Reisman and Ahamed, \{Sheikh Iqbal\}",

booktitle = "Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020",

address = "United States",

}

Abdul Basit Ur Rahim, M, Duan, Q & Al-Shaer, E 2020, A Formal Analysis of Moving Target Defense. in WK Chan, B Claycomb, H Takakura, J-J Yang, Y Teranishi, D Towey, S Segura, H Shahriar, S Reisman & SI Ahamed (eds), Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020., 9202451, Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020, Institute of Electrical and Electronics Engineers Inc., pp. 1802-1807, 44th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2020, Virtual, Madrid, Spain, 13/07/20. https://doi.org/10.1109/COMPSAC48688.2020.00050

A Formal Analysis of Moving Target Defense. / Abdul Basit Ur Rahim, Muhammad; Duan, Qi; Al-Shaer, Ehab.
Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020. ed. / W. K. Chan; Bill Claycomb; Hiroki Takakura; Ji-Jiang Yang; Yuuichi Teranishi; Dave Towey; Sergio Segura; Hossain Shahriar; Sorel Reisman; Sheikh Iqbal Ahamed. Institute of Electrical and Electronics Engineers Inc., 2020. p. 1802-1807 9202451 (Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020).

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

TY - GEN

T1 - A Formal Analysis of Moving Target Defense

AU - Abdul Basit Ur Rahim, Muhammad

AU - Duan, Qi

AU - Al-Shaer, Ehab

PY - 2020/7

Y1 - 2020/7

N2 - Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.

AB - Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.

KW - Formal specification

KW - Moving target defense

KW - configuration-based mutation

KW - model checking

KW - verification

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

U2 - 10.1109/COMPSAC48688.2020.00050

DO - 10.1109/COMPSAC48688.2020.00050

M3 - Conference contribution

AN - SCOPUS:85094112261

T3 - Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020

SP - 1802

EP - 1807

BT - Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020

A2 - Chan, W. K.

A2 - Claycomb, Bill

A2 - Takakura, Hiroki

A2 - Yang, Ji-Jiang

A2 - Teranishi, Yuuichi

A2 - Towey, Dave

A2 - Segura, Sergio

A2 - Shahriar, Hossain

A2 - Reisman, Sorel

A2 - Ahamed, Sheikh Iqbal

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 44th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2020

Y2 - 13 July 2020 through 17 July 2020

ER -

Abdul Basit Ur Rahim M, Duan Q, Al-Shaer E. A Formal Analysis of Moving Target Defense. In Chan WK, Claycomb B, Takakura H, Yang JJ, Teranishi Y, Towey D, Segura S, Shahriar H, Reisman S, Ahamed SI, editors, Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020. Institute of Electrical and Electronics Engineers Inc. 2020. p. 1802-1807. 9202451. (Proceedings - 2020 IEEE 44th Annual Computers, Software, and Applications Conference, COMPSAC 2020). doi: 10.1109/COMPSAC48688.2020.00050

A Formal Analysis of Moving Target Defense

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this