Formal design of communication checkers for ICCP using UPPAAL

Salman Malik, Robin Berthier, Rakesh B. Bobba, Roy H. Campbell, William H. Sanders

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Vulnerabilities in key communication protocols that drive the daily operations of the power grid may lead to exploits that could potentially disrupt its safety-critical operation and may result in loss of power, consequent financial losses, and disruption of crucial power-dependent services. This paper focuses on the Inter Control Center Communications Protocol, (ICCP), which is the protocol used among control centers for data exchange and control. We discuss use of UPPAAL in formal modeling of portions of ICCP. Specifically, we present an iterative process and framework for the design and formal verification of tailored checking mechanisms that protect resource-exhaustion vulnerabilities in the protocol standard from attacks and exploits. We discuss insights we gained and lessons we learned when modeling the protocol functionalities and running the UPPAAL model checker to prove critical security and safety properties, and we discuss the overall success of this approach.

Original languageEnglish (US)
Title of host publication2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013
Pages486-491
Number of pages6
DOIs
StatePublished - Dec 1 2013
Event2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 - Vancouver, BC, Canada
Duration: Oct 21 2013Oct 24 2013

Publication series

Name2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013

Other

Other2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013
CountryCanada
CityVancouver, BC
Period10/21/1310/24/13

Fingerprint

Network protocols
Communication
Electronic data interchange

ASJC Scopus subject areas

  • Hardware and Architecture

Cite this

Malik, S., Berthier, R., Bobba, R. B., Campbell, R. H., & Sanders, W. H. (2013). Formal design of communication checkers for ICCP using UPPAAL. In 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 (pp. 486-491). [6688005] (2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013). https://doi.org/10.1109/SmartGridComm.2013.6688005

Formal design of communication checkers for ICCP using UPPAAL. / Malik, Salman; Berthier, Robin; Bobba, Rakesh B.; Campbell, Roy H.; Sanders, William H.

2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013. 2013. p. 486-491 6688005 (2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Malik, S, Berthier, R, Bobba, RB, Campbell, RH & Sanders, WH 2013, Formal design of communication checkers for ICCP using UPPAAL. in 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013., 6688005, 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013, pp. 486-491, 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013, Vancouver, BC, Canada, 10/21/13. https://doi.org/10.1109/SmartGridComm.2013.6688005
Malik S, Berthier R, Bobba RB, Campbell RH, Sanders WH. Formal design of communication checkers for ICCP using UPPAAL. In 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013. 2013. p. 486-491. 6688005. (2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013). https://doi.org/10.1109/SmartGridComm.2013.6688005
Malik, Salman ; Berthier, Robin ; Bobba, Rakesh B. ; Campbell, Roy H. ; Sanders, William H. / Formal design of communication checkers for ICCP using UPPAAL. 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013. 2013. pp. 486-491 (2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013).
@inproceedings{386f725606514df3a375cfe6d5be95dd,
title = "Formal design of communication checkers for ICCP using UPPAAL",
abstract = "Vulnerabilities in key communication protocols that drive the daily operations of the power grid may lead to exploits that could potentially disrupt its safety-critical operation and may result in loss of power, consequent financial losses, and disruption of crucial power-dependent services. This paper focuses on the Inter Control Center Communications Protocol, (ICCP), which is the protocol used among control centers for data exchange and control. We discuss use of UPPAAL in formal modeling of portions of ICCP. Specifically, we present an iterative process and framework for the design and formal verification of tailored checking mechanisms that protect resource-exhaustion vulnerabilities in the protocol standard from attacks and exploits. We discuss insights we gained and lessons we learned when modeling the protocol functionalities and running the UPPAAL model checker to prove critical security and safety properties, and we discuss the overall success of this approach.",
author = "Salman Malik and Robin Berthier and Bobba, {Rakesh B.} and Campbell, {Roy H.} and Sanders, {William H.}",
year = "2013",
month = "12",
day = "1",
doi = "10.1109/SmartGridComm.2013.6688005",
language = "English (US)",
isbn = "9781479915262",
series = "2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013",
pages = "486--491",
booktitle = "2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013",

}

TY - GEN

T1 - Formal design of communication checkers for ICCP using UPPAAL

AU - Malik, Salman

AU - Berthier, Robin

AU - Bobba, Rakesh B.

AU - Campbell, Roy H.

AU - Sanders, William H.

PY - 2013/12/1

Y1 - 2013/12/1

N2 - Vulnerabilities in key communication protocols that drive the daily operations of the power grid may lead to exploits that could potentially disrupt its safety-critical operation and may result in loss of power, consequent financial losses, and disruption of crucial power-dependent services. This paper focuses on the Inter Control Center Communications Protocol, (ICCP), which is the protocol used among control centers for data exchange and control. We discuss use of UPPAAL in formal modeling of portions of ICCP. Specifically, we present an iterative process and framework for the design and formal verification of tailored checking mechanisms that protect resource-exhaustion vulnerabilities in the protocol standard from attacks and exploits. We discuss insights we gained and lessons we learned when modeling the protocol functionalities and running the UPPAAL model checker to prove critical security and safety properties, and we discuss the overall success of this approach.

AB - Vulnerabilities in key communication protocols that drive the daily operations of the power grid may lead to exploits that could potentially disrupt its safety-critical operation and may result in loss of power, consequent financial losses, and disruption of crucial power-dependent services. This paper focuses on the Inter Control Center Communications Protocol, (ICCP), which is the protocol used among control centers for data exchange and control. We discuss use of UPPAAL in formal modeling of portions of ICCP. Specifically, we present an iterative process and framework for the design and formal verification of tailored checking mechanisms that protect resource-exhaustion vulnerabilities in the protocol standard from attacks and exploits. We discuss insights we gained and lessons we learned when modeling the protocol functionalities and running the UPPAAL model checker to prove critical security and safety properties, and we discuss the overall success of this approach.

UR - http://www.scopus.com/inward/record.url?scp=84893635510&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84893635510&partnerID=8YFLogxK

U2 - 10.1109/SmartGridComm.2013.6688005

DO - 10.1109/SmartGridComm.2013.6688005

M3 - Conference contribution

AN - SCOPUS:84893635510

SN - 9781479915262

T3 - 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013

SP - 486

EP - 491

BT - 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013

ER -