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 language | English (US) |
|---|---|
| Title of host publication | 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 |
| Pages | 486-491 |
| Number of pages | 6 |
| DOIs | |
| State | Published - Dec 1 2013 |
| Event | 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 - Vancouver, BC, Canada Duration: Oct 21 2013 → Oct 24 2013 |
Publication series
| Name | 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 |
|---|
Other
| Other | 2013 IEEE International Conference on Smart Grid Communications, SmartGridComm 2013 |
|---|---|
| Country | Canada |
| City | Vancouver, BC |
| Period | 10/21/13 → 10/24/13 |
Fingerprint
ASJC Scopus subject areas
- Hardware and Architecture
Cite this
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 proceeding › Conference contribution
}
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 -