IOT: Formal Security Analysis of Smart Embedded Systems

Smart embedded systems are core components of Internet of Things (IoT).
Many vulnerabilities and attacks have been discovered against
different classes of IoT devices. Therefore, developing a systematic
mechanism to analyze the security of smart embedded systems
will help developers discover new attacks,
and improve the design and implementation of the system.
In this paper, we formally model the functionalities
of smart meters, as an example of a widely used smart embedded device, using rewriting logic. We also define a formal
set of actions for attackers.
Our formal model enables us to
automatically analyze the system, and using model-checking,
find all the sequences of attacker actions that
transition the system to any undesirable state. We evaluate the
analysis results of our model on a real smart meter, and
find that a sizeable set of the attacks found by the model
can be applied to the real meter, using only inexpensive, commodity off-the-shelf hardware.

Author(s):

Farid Molazem    
University of British Columbia
Canada

Karthik Pattabiraman    
University of British Columbia
Canada