Open Collections

UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Security analysis and intrusion detection for embedded systems : a case study of smart meters Molazem Tabrizi, Farid 2017

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Notice for Google Chrome users:
If you are having trouble viewing or searching the PDF with Google Chrome, please download it here instead.

Item Metadata


24-ubc_2017_november_molazemtabrizi_farid.pdf [ 20.01MB ]
JSON: 24-1.0357148.json
JSON-LD: 24-1.0357148-ld.json
RDF/XML (Pretty): 24-1.0357148-rdf.xml
RDF/JSON: 24-1.0357148-rdf.json
Turtle: 24-1.0357148-turtle.txt
N-Triples: 24-1.0357148-rdf-ntriples.txt
Original Record: 24-1.0357148-source.json
Full Text

Full Text

Security Analysis and IntrusionDetection for Embedded SystemsA Case Study of Smart MetersbyFarid Molazem TabriziB.Sc., Amirkabir University of Technology, 2005M.Sc., Simon Fraser University, 2011A THESIS SUBMITTED IN PARTIAL FULFILLMENT OFTHE REQUIREMENTS FOR THE DEGREE OFDOCTOR OF PHILOSOPHYinThe Faculty of Graduate and Postdoctoral Studies(Electrical & Computer Engineering)THE UNIVERSITY OF BRITISH COLUMBIA(Vancouver)October 2017c© Farid Molazem Tabrizi 2017AbstractEmbedded systems are widely used in critical situations and hence, are tar-gets for malicious users. Researchers have demonstrated successful attacksagainst embedded systems used in power grids, modern cars, and medicaldevices. Hence, it is imperative to develop techniques to improve securityof these devices. However, embedded devices have constraints (such as lim-ited memory capacity) that make building security mechanisms for themchallenging.In this thesis, we formulate building Intrusion Detection System (IDS)for embedded systems as an optimization problem. We develop algorithmsthat, given the set of the security properties of the system and the invariantsthat verify those properties, build an IDS that maximizes the coverage forthe security properties, with respect to the available memory. This allowsour IDS to be applicable to a wide range of embedded devices with differentmemory capacities. Furthermore, we develop techniques to analyze securityof both design and implementation of embedded systems. Given a set ofcapabilities of attackers, we automatically analyze the system and identifyways an adversary may tamper with the system. This will help developersdiscover new attacks, and improve the design and implementation of thesystem.iiLay SummaryEmbedded systems are widely used in critical situations and hence, are tar-gets for malicious users. Researchers have demonstrated successful attacksagainst embedded systems used in power grids, modern cars, and medicaldevices. Hence, it is imperative to develop techniques to improve security ofthese devices. However, embedded devices have constraints (such as limitedmemory capacity) that make building security mechanisms for them chal-lenging. Moreover, embedded systems have proximity to users. This allowsthe attackers to, compared to general purpose computers, have extendedaccess to them, and makes their security analysis challenging.In this thesis, we propose techniques to build light-weight Intrusion De-tection System that is optimized for constraints of embedded devices. Also,we propose security analysis solutions that is customized for the threat modelembedded systems have.iiiPrefaceThis thesis is the result of work carried out by myself, in collaboration withmy advisor, Dr. Karthik Pattabiraman. Chapters 3, 4, and 5 are based onwork published in various workshops and conferences, and a paper submittedto a journal. I was responsible for writing all the papers, designing solutions,conducting the experiments and evaluating the results. My advisor wasresponsible for editing and writing segments of the manuscripts, providingfeedback and guidance during design phases, experiments, and evaluations.Below are publication details for each chapter:• Chapter 3:– ”a Model-Based Intrusion Detection System For Smart Meters”Farid Molazem Tabrizi and Karthik Pattabiraman, in the Pro-ceedings of the IEEE International Symposium on High-AssuranceSystems Engineering (HASE), 2014.– ”a Model For Security Analysis of Smart Meters” Farid MolazemTabrizi and Karthik Pattabiraman, Workshop on Recent Ad-vances in Intrusion Tolerance and reSilience (WRAITS), 2012.• Chapter 4:– ”Flexible Intrusion Detection System For Memory-ConstrainedEmbedded Systems” Farid Molazem Tabrizi and Karthik Pat-tabiraman, Proceedings of the 11th European Dependable Com-puting Conference (EDCC), 2015.– ”Optimizing Intrusion Detection Systems For Memory-ConstrainedEmbedded Systems” Farid Molazem Tabrizi and Karthik Pattabi-raman, Submitted to a Journal.ivPreface• Chapter 5:– ”Formal Security Analysis of Smart Meters” Farid Molazem Tabrizi,Karthik Pattabiraman, 32nd Annual Computer Security Appli-cations Conference (ACSAC) 2016.– ”Design-Level and Code-Level Security Analysis of IoT Devices”Farid Molazem Tabrizi, Karthik Pattabiraman, Under prepara-tion for submission.vTable of ContentsAbstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiLay Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iiiPreface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ivTable of Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . viList of Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ixList of Figures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xList of Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . xivAcknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . xv1 Introduction and Overview . . . . . . . . . . . . . . . . . . . . 11.1 Embedded systems . . . . . . . . . . . . . . . . . . . . . . . 11.2 Constraints of embedded systems . . . . . . . . . . . . . . . 21.3 Platform . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.4 Threat model . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.5 Research questions . . . . . . . . . . . . . . . . . . . . . . . . 51.6 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . 71.7 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102.1 Intrusion detection systems . . . . . . . . . . . . . . . . . . . 112.2 Security analysis . . . . . . . . . . . . . . . . . . . . . . . . . 14viTable of Contents2.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173 Low-memory Intrusion Detection System for Embedded Sys-tems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183.1 Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183.1.1 Abstract and concrete models . . . . . . . . . . . . . 203.1.2 System call selection and state machine generation . 223.1.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . 243.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263.2.1 Experimental setup . . . . . . . . . . . . . . . . . . . 263.2.2 Results . . . . . . . . . . . . . . . . . . . . . . . . . . 283.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324 Optimizing Intrusion Detection System for Embedded Sys-tems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 344.1 Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 344.1.1 Problem formulation . . . . . . . . . . . . . . . . . . 354.1.2 System overview . . . . . . . . . . . . . . . . . . . . . 374.1.3 Details . . . . . . . . . . . . . . . . . . . . . . . . . . 384.1.4 Building the model . . . . . . . . . . . . . . . . . . . 404.1.5 Optimizations . . . . . . . . . . . . . . . . . . . . . . 474.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 544.2.1 Experimental setup . . . . . . . . . . . . . . . . . . . 554.2.2 Experiments . . . . . . . . . . . . . . . . . . . . . . . 554.2.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . 574.3 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 655 Security Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 675.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . 685.1.1 Characteristics of embedded devices . . . . . . . . . . 685.1.2 Security invariants . . . . . . . . . . . . . . . . . . . . 695.2 Design-level analysis . . . . . . . . . . . . . . . . . . . . . . . 695.2.1 Rewriting logic . . . . . . . . . . . . . . . . . . . . . . 715.2.2 Formal model . . . . . . . . . . . . . . . . . . . . . . 72viiTable of Contents5.2.3 Attacker model . . . . . . . . . . . . . . . . . . . . . 765.3 Code-level analysis . . . . . . . . . . . . . . . . . . . . . . . . 795.3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . 805.3.2 Problem formulation . . . . . . . . . . . . . . . . . . 815.3.3 Step 1: code transformation . . . . . . . . . . . . . . 825.3.4 Step 2: finding attacks . . . . . . . . . . . . . . . . . 845.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 875.4.1 Research questions . . . . . . . . . . . . . . . . . . . 875.4.2 Testbed . . . . . . . . . . . . . . . . . . . . . . . . . . 875.4.3 Performance (RQ2.1) . . . . . . . . . . . . . . . . . . 885.4.4 Comprehensiveness (RQ2.2) . . . . . . . . . . . . . . 915.4.5 Mounting the attacks . . . . . . . . . . . . . . . . . . 1035.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1056 Conclusion and Future Work . . . . . . . . . . . . . . . . . . 1096.1 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1096.2 Expected impact . . . . . . . . . . . . . . . . . . . . . . . . . 1116.3 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1126.4 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . 1136.5 Final words . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117viiiList of Tables3.1 Running time overhead of our model-based technique andcomplete-system-calls technique. . . . . . . . . . . . . . . . . 293.2 Code injection detection coverage of our technique Versusother techniques for each sub-system of the meter . . . . . . . 304.1 Abstract invariants for an execution path of smart meter. . . 404.2 Availability and integrity properties of SegMeter. . . . . . . . 564.3 Effects of fault injection on the smart meter software. . . . . 575.1 Accesses and capabilities of the adversary . . . . . . . . . . . 685.2 Performance of model checker for different attacks . . . . . . 895.3 Analysis time . . . . . . . . . . . . . . . . . . . . . . . . . . . 905.4 Assertions used for SEGMeter . . . . . . . . . . . . . . . . . . 104ixList of Figures1.1 High-level representation of defense layers for embedded sys-tems. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23.1 Concrete model for portion of the abstract model . . . . . . . 223.2 The state machine based on the concrete model: here thesequence time socket* write represents the flow of this smallsection of the concrete model. . . . . . . . . . . . . . . . . . . 243.3 SEGMeter: our open source meter testbed. The board on theleft is the gateway board in charge of communicating with theserver, and the board on the right is the Arduino board thatreceives consumption data from the sensors. . . . . . . . . . . 273.4 CPU overhead for different monitoring time values (T ). . . . 334.1 An execution path of smart meter operations used as a run-ning example. . . . . . . . . . . . . . . . . . . . . . . . . . . . 354.2 Formulation of the IDS as an optimization problem. . . . . . 354.3 We convert functions into automaton connectives throughstatic analysis and then into concrete invariants. The labelson state transitions correspond to the system calls executedin the code. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424.4 The invariants v1 to v6 verify the properties p1 to p4. . . . . . 424.5 We allow ranking relationship between invariants of the sys-tem. An invariant may not be included in the IDS unless allthe invariants of higher rank are also included. . . . . . . . . 52xList of Figures4.6 We have categorized the fault injection results into 7 cate-gories. The statistics of occurrences of each of these categoriesare presented in this figure. . . . . . . . . . . . . . . . . . . . 574.7 The detection results of MaxMinCoverage IDS built using4MB of memory, for attacks against different security prop-erties of SEGMeter. . . . . . . . . . . . . . . . . . . . . . . . 574.8 The accuracy of MaxMinCoverage IDS built using 4MB ofmemory for different security properties of SEGMeter. . . . 584.9 The detection results of MaxProperty IDS built using 4MBof memory, for attacks against different security properties ofSEGMeter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 584.10 The accuracy of MaxMinCoverage IDS built using 4MB ofmemory for different security properties of SEGMeter. . . . 584.11 Performance overhead of MaxMinCoverage IDS and Max-Property IDS using different time intervals. Making the timeinterval too small will increase the performance overhead. . . 624.12 The detection results of MaxMinCoverage IDS built using2MB of memory, for attacks against security properties ofSEGMeter. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 624.13 The accuracy of MaxMinCoverage IDS built using 2MB ofmemory, for security properties of SEGMeter. . . . . . . . . 634.14 The detection results of MaxProperty IDS built using 2MBof memory, for different security properties of SEGMeter. . . 634.15 The accuracy of MaxProperty IDS using 2MB of memory,for different security properties of SEGMeter. . . . . . . . . 634.16 The detection results of MaxMinCoverage IDS after invariantreduction, and using 4MB of memory. . . . . . . . . . . . . . 644.17 The detection results of MaxMinCoverage IDS after invariantreduction, and using 2MB of memory. . . . . . . . . . . . . . 644.18 The detection results of MaxProperty IDS after invariant re-duction, and using 4MB of memory. . . . . . . . . . . . . . . 644.19 The detection results of MaxProperty IDS after invariant re-duction, and using 2MB of memory. . . . . . . . . . . . . . . 64xiList of Figures4.20 The detection results of MaxMinCoverage IDS in the presenceof invariant ranking, and using 2MB of memory. . . . . . . . 644.21 The detection results of MaxProperty IDS in the presence ofinvariant ranking, and using 2MB of memory. . . . . . . . . 645.1 In this section, we discuss and formalize the first two execu-tion paths of the smart meter, shown in this figure. . . . . . . 735.2 SensorList is a series of SensorElements and is the result ofmicrocontroller operations. . . . . . . . . . . . . . . . . . . . 745.3 Formal model of sensor data in Maude. . . . . . . . . . . . . 745.4 Formal model of states of sensor data in Maude. . . . . . . . 755.5 Formal model of receiving sensor data from the microcontroller. 765.6 SensorList is a series of SensorElements and is the result ofmicrocontroller operations. . . . . . . . . . . . . . . . . . . . 775.7 Formal model of storing sensor data received from the micro-controller. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 775.8 Formal model of the attacker actions. . . . . . . . . . . . . . 795.9 Overview of our technique to find software-interference at-tacks against the system. . . . . . . . . . . . . . . . . . . . . 815.10 High-level representation of attacker action injection in thecode. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 835.11 ’alt request()’ represents action of an attacker that is capableof dropping http response messages. . . . . . . . . . . . . . . 855.12 By symbolically executing the code, we find out how attackeractions may lead to violating security invariants in the code. . 865.13 The abstract model for updating sensor data file. . . . . . . . 945.14 We used a programmable solid state timer for rebooting thesystem at precise times, and a USB-to-Serial cable to mountreplay attack on the meter. . . . . . . . . . . . . . . . . . . . 955.15 SEGMeter code for updating sensor data file. The commentsare added by us to show the mapping with the states in Fig. 5.13. 955.16 Time synchronization code for SEGMeter. . . . . . . . . . . . 96xiiList of Figures5.17 SEGMeter code for communicating with the sensors on thesmart meter. The comments are added by us to show themapping with the states in Fig. 5.19. . . . . . . . . . . . . . 975.18 The abstract model for time synchronization. The dottedlines are added by the attacker. . . . . . . . . . . . . . . . . . 985.19 The abstract model for sensor communication . . . . . . . . . 1005.20 The functions defining dropping messages, replaying mes-sages, and rebooting the system. . . . . . . . . . . . . . . . . 1065.21 Partial code that represents calculating parts of electricityconsumption data and storing them in the buffer. . . . . . . . 1075.22 Code snippet for reading data from the serial interface. . . . . 1075.23 Code snippet representing receiving and storing site token. . 108xiiiList of Algorithms1 Algorithm for building the IDS . . . . . . . . . . . . . . . . . . 452 Algorithm for invariant reduction. . . . . . . . . . . . . . . . . 503 Finding optimal IDS, given the memory constraint and theranking relationships between the invariants. . . . . . . . . . . 53xivAcknowledgmentsFirstly, I would like to express my sincere gratitude to my PhD advisor, Prof.Karthik Pattabiraman. If it was not for your continuous support, carefulguidance, and great patience, I would not have been able to complete thisthesis today. Your advice on my research and career has been invaluable,and has helped me grow both as a researcher, and as a person.Besides my advisor, I would like to thank my thesis committe and exam-iners, including Prof. Ali Mesbah, and Prof. Sathish Gopalakrishnan. Youprovided me with valuable feedback, and helped me improve my thesis. Iwould like to give special thanks to all my colleagues at Dependable SystemsLab for the stimulating discussions, and all the joy we had working together.The memories will stay with me forever.Thanks to my colleagues at CSRG, including Prof. Matei Ripeanu, forinteresting weekly readings we had, and constructive feedback on my re-search and practice presentations, over the years.Since starting my PhD and living in Vancouver, I formed precious friend-ships. Thanks to all my friends for making these years as joyful as possible,and supporting me through ups and downs. In the end, I want to thank myfamily and relatives. My loving parents, you have supported me uncondi-tionally, and beyond imagination. You shaped me into who I am today, andI will be forever grateful to you. My two brothers, you have always beenthere for me whenever I needed you. I am very lucky to have you in my life.Finally, thanks to my relatives, for being a constant source of energy andmoral support for me.xvChapter 1Introduction and Overview1.1 Embedded systemsEmbedded systems are computing devices that are designed to perform spe-cific set of tasks. The use of embedded systems in our daily lives is growingrapidly. Smart home solutions use embedded systems that control lighting,appliances and entertainment systems. Modern cars use a network of thesedevices to control speed, brakes and navigation. Embedded systems areused as implantable medical devices such as pacemakers and insulin pumps.They are used in smart grids in the form of smart meters. These metersare key components of the grid and their annual deployment is projected toreach 180 million by 2018 [47].Modern embedded systems carry out sensitive tasks. They are alsoequipped with various network interfaces and communicate with each other.This increases their attack surface. Given the sensitivity of their applicationand their extended attack surface, these systems are targets for security at-tacks. Researchers have successfully demonstrated vulnerabilities in variousclasses of embedded systems [32, 48, 50, 54, 56, 87]. These demonstrate theneed for techniques to improve the security of modern embedded systems.Figure 1.1 illustrates the high-level representation of defense layers fornetworked embedded devices. We classify these security techniques intonetwork-based and host-based. Network-based techniques isolate networkeddevices against attacks. These mechanisms, including Network-based In-trusion Detection Systems (IDS) and Firewalls, may have false negativesand hence, do not guarantee protection of hosts against attacks. Therefore,developing host-based security techniques is a necessary step for providingdefense-in-depth for such devices. The first host-based defense layer is a se-11.2. Constraints of embedded systemsIDSharden	the	embedded	softwareNetworkFirewallNetwork	IDSEmbedded	deviceRQ1:First	line	of	defenseRQ2:	Second	line	of	defenseHost	security Network	securityFigure 1.1: High-level representation of defense layers for embedded systems.curity mechanism such as a host-based IDS. This defense layer addresses theattacks that are not caught via network-based security techniques. However,host-based IDSes may have false negatives as well. Therefore, we consideranalyzing the security of the embedded system’s software as another layerof defense for hardening the host and providing host-based security. Thisway, even if an attack evades the host-based IDS, it may not tamper withthe software.The goal of this thesis is developing the two layers of host-based secu-rity for embedded devices. In the remainder of this chapter, we discuss thelimitations of modern embedded devices that make developing security so-lutions for them challenging. Later, we introduce the platform we use toevaluate our work, and finally, we lay out the research questions this thesisis addressing.1.2 Constraints of embedded systemsUnlike general purpose computers, many modern embedded devices are con-strained in terms of computing power, memory, cost, etc. We list the keyconstraints that security mechanisms must satisfy to be applicable to thesedevices:21.2. Constraints of embedded systems1. Performance: Many embedded devices are low-end computing ma-chines. Memory and computation overhead are therefore, significantlimiting factors. For example, an important component of a securitymechanism such as an IDS is a model that represents the correct be-havior of the software and/or a set of malicious behavior signatures.This model may occupy a large space in memory. However, many em-bedded devices have limited memory capacity and this makes a bodyof existing security techniques inapplicable to them [36, 83].2. No false positives: False positive happens when a security mechanismreports an attack, while no actual attack has occurred. Many embed-ded systems are deployed on a large scale and communicate with aserver. Even a very small false positive rate will result in rapid ag-gregation of false alarms which imposes large overhead on the server.For example, IDSes typically target the false positive rate of 1% [44].However, even a false positive rate of 0.5% over a full-day audit tracefor 500,000 devices, means handling 2500 daily false positives for theserver. Therefore, it is important to have no false positives.3. Software modification: Many embedded systems must meet certainreal-time properties. For example, software running on smart metersmust read consumption data from sensors in real-time and maintaina two-way communication with the server. Any security mechanismthat modifies the software and changes its real-time behavior is notacceptable for these devices.4. Low cost: Since many embedded systems such as smart meters andimplantable medical devices are deployed on a large scale, any extracost for individual systems incurs large financial overhead to the wholesystem. For instance, adding a $10 memory chip to the smart metersin the grid adds up to $10 million extra cost when the meters aredeployed for one million homes and businesses. Hence, cost is animportant constraint for embedded systems, and indirectly affects theirperformance.31.3. Platform5. Coverage of unknown attacks: Modern embedded systems are fairlynew systems and are currently being deployed around the world in thecontext of Internet of Things. Therefore, their attack vectors are notwell-studied. Considering this, any security mechanism developed forthem must have the ability to detect unknown attacks.1.3 PlatformSmart meters are networked embedded systems. They are key componentsof the smart grid and will be installed at homes and businesses, calculatepower consumption, and provide a two-way communication with the util-ity provider. The annual deployment of smart meters is projected to reach180 million by 2018 [47]. The large-scale deployment of smart meters inthe world, and the criticality of their operations make them an interestingtestbed for us to evaluate our work. Therefore, we use smart meters as eval-uation platform in this thesis. Smart meters have three main components,as we explain below.Control unit: Inside the meter, there is a Microcontroller that trans-fers data measured by the low-level meter engine to a flash memory. TheMicrocontroller can save logs of important events during the activity of thesmart meter.Communication unit: For the meters to be able to communicate witheach other and the server, they are equipped with a Network Interface Card(NIC). Meters can be connected to in-home displays, programmable control-lable thermostats, etc. to form a Home Area Network (HAN). In each area,smart meters will be connected to a collector through field area network(FAN). This collector gathers all data and communicates with the utilityserver through Wide Area Network (WAN). The communication interfacediffers from region to region.Clock: For the meters to have the capability of providing time-of-usebilling services, they are equipped with a real-time clock (RTC). This clockshould be synchronized with the server clock on a regular basis to preventany drift. This is done through synchronization messages.41.4. Threat model1.4 Threat modelIn this thesis, we assume that the goal of the adversary is to change thenormal execution path of the software running on the embedded device.This may be to achieve economic benefits, for example a malicious user maytamper with a smart metering device to pay less money for consumed power.To achieve this goal, the adversary may take advantage of access to system’scommunication interfaces, sensors, power source, etc., and perform actionssuch as dropping messages, and spoofing sensor data. The attacker’s actionschange the control flow of the software and impact its functionality.The attacker stated above is designed based on the characteristics ofembedded devices which allows the users to physically interact with themand access their components, e.g., communication interfaces. This is unlikeattacks against remote servers where physical access is very limited. There-fore, we define a new term for these attacks. We call the attacks resultingfrom such interactions (e.g., the ones stated in the attacker model above),which lead to corrupting data [21] of the software and/or violating its con-trol flow [6], as software-interference attacks. We consider this category ofattacks in this thesis. To the best of our knowledge, there is no existingterm for these attacks, which is why we coined a new term.We do not consider social engineering attacks, attacks on confidentiality,and denial of service (DoS) attacks. The reason is that these attacks aregenerally addressed by other techniques such as network security measures,cryptographic methods, and Human-Computer Interaction analysis/socialstudies.1.5 Research questionsThe overall goal of this thesis is to develop host-based defense layers forembedded systems. We consider building a host-based IDS to be the firstdefense layer, and hardening the embedded systems’ software via securityanalysis to be the second defense layer. Given the constraints of embeddedsystems discussed in this chapter, and to address the goal of this thesis,51.5. Research questionswe lay out three research questions. The first two questions account fordeveloping host-based IDS for embedded systems, and the third questionaddresses analyzing security of these devices:• RQ1.1. How can we reduce resource requirements of a host-based intrusion detection system for embedded systems? Em-bedded systems have resource constraints. Therefore, we developed amethod to selectively monitor the components of the system that aremore likely to be target of attacks, according to an attack taxonomy.This allows us to reduce memory requirements of the IDS while pro-viding coverage for critical components of the system.• RQ1.2. How can we optimize a host-based Intrusion Detec-tion System for embedded system, with respect to availableresources? We generalized our method developed for RQ1.1, to op-timize the provided security. We automatically produce an IDS thatprovides maximum coverage with respect to user-defined criteria andavailable memory.• RQ2. How can we automatically analyze security of embed-ded systems with respect to the extended accesses the ad-versaries have to them? Existing techniques for analyzing securityof computer systems either rely on previous knowledge of vulnerabil-ities and attack databases developed for general purpose computers,or use methods such as fuzzing. Hence, existing techniques do notaccount for unique attack surface of embedded systems (see Chapter1.4) compared to general purpose computers. To address this problem,we took advantage of the fact that embedded systems are designed toperform specific set of tasks. Based on that: 1) Using rewriting logic[59], we built a formal model of a class of embedded systems, namelysmart meters, along with a set of attacker actions developed based onaccesses adversaries may have to the these systems. This allows us toautomatically analyze the design of this class of devices, 2) we devel-oped a technique to inject code snippets representing attacker actions61.6. Contributionsin the software of embedded devices. We used symbolic execution tofind all possible ways an attacker may affect the system at run-time,and mount an attack. As a result, we were able to automatically an-alyze both design and implementation of embedded systems based ontheir attack surface.1.6 ContributionsIn this thesis, we make the following contributions:• In Chapter 3, we introduce an algorithm to build an IDS that incurslow memory overhead via partial-monitoring of the system calls ofthe software running on smart meters. In our evaluations, we demon-strate that our algorithm successfully detects 70% of attacks on thesystem, while monitoring only 30% of the system calls. Moreover, weshow that partial-monitoring resulting from heuristics such as pickingfrequent system calls, provides detection rate of about 36%, which issignificantly lower than our algorithm’s detection rate. This indicatesthat our proposed approach is an effective way of building IDS forembedded devices that have memory constraints.• In Chapter 4, we extend our solution from Chapter 3. We propose aflexible technique to automatically build IDSes optimized for availablememory. The user may define their own optimization criteria. Thismakes our solution applicable to a wide range of embedded systems.Moreover, we propose two optimization criteria, and design/implementIDSes based on them. We evaluate our IDSes on an open source smartmeter, based on their detection rates, compliance of their detectionrates with their estimated coverage at design time, and their perfor-mance overheads. Our results confirm that, using our technique, thedevelopers may build an IDS customized for the memory constraints oftheir device. For example, on our testbed, using only a small portionof the memory required to build a complete IDS, the developer mayautomatically build an IDS that can effectively distribute the cover-71.7. Publicationsage among all security properties, with a minimum of 70% detectionrate. Hence, our technique: 1) provides a flexible mechanism to buildoptimized IDSes with respect to memory constraints, and 2) providesinformation regarding expected performance of IDS in detecting at-tacks. Therefore, developers may make informed decisions regardingthe security of their system (e.g., adding more memory resources ifnecessary).• In Chapter 5, we propose an automated technique to find software-interference attacks (see Chapter 1.4) against embedded devices, basedon an attacker model. Our technique allows the users to, within thespace of the model, search all the ways an attacker may interact withthe system, and find the ones that break security invariants of the de-vice. Our technique does not rely on existing attack databases. It isalso flexible with respect to the attacker model, i.e., new capabilitiesfor the attacker may be added or removed from it based on the prop-erties of the system. We evaluate our work on an open-source smartmeter. We find over 9 different types of software-interference attacks,and over 50 ways to mount the attacks on the system. Using off-the-shelf, inexpensive equipment, we experimentally validate the attacksfound on our testbed. This indicates that our technique is useful asit finds realistic attacks. Also, the users of our technique may fix thediscovered vulnerabilities and improve the security of the device.1.7 PublicationsTo address the research questions discussed in Chapter 1.5, we have pub-lished the following papers:• RQ1.1: ”A MODEL-BASED INTRUSION DETECTION SYSTEMFOR SMART METERS” Farid Molazem Tabrizi and Karthik Pat-tabiraman, in the Proceedings of the IEEE International Symposiumon High-Assurance Systems Engineering (HASE), 2014 (Acceptancerate 30%).81.7. Publications• RQ1.1: ”A MODEL FOR SECURITY ANALYSIS OF SMART ME-TERS” Farid Molazem Tabrizi and Karthik Pattabiraman, Workshopon Recent Advances in Intrusion Tolerance and reSilience (WRAITS),2012.• RQ1.2: ”FLEXIBLE INTRUSION DETECTION SYSTEMS FORMEMORY-CONSTRAINED EMBEDDED SYSTEMS” Farid MolazemTabrizi and Karthik Pattabiraman, Proceedings of the 11th EuropeanDependable Computing Conference (EDCC), 2015. (Acceptance rate:45%) Distinguished paper award.• RQ1.2: ”OPTIMIZING INTRUSION DETECTION SYSTEMS FORMEMORY-CONSTRAINED EMBEDDED SYSTEMS” Farid MolazemTabrizi and Karthik Pattabiraman, Submitted to Transactions on Em-bedded Computing Systems, 2017.• RQ2: ”FORMAL SECURITY ANALYSIS OF SMART METERS”Farid Molazem Tabrizi, Karthik Pattabiraman, 32nd Annual Com-puter Security Applications Conference (ACSAC) 2016. (Acceptancerate 23%)• RQ2: ”DESIGN-LEVEL AND CODE-LEVEL SECURITY ANALY-SIS OF IoT DEVICES” Farid Molazem Tabrizi, Karthik Pattabira-man, Under preparation for submission.9Chapter 2Related WorkIn the first section of this chapter, we discuss prior research in building In-trusion Detection Systems. We study techniques based on machine learning,static analysis, and hardware modules. These techniques are widely used forgeneral purpose computers and may potentially be applicable to embeddedsystems as well. Therefore, we review them and explain why constraints ofembedded systems make application of these solutions to them, challenging.In the second section of this chapter, we review techniques for analyzingsecurity of software systems. These techniques include attack trees, attackpatterns, attack graphs, fault injection, and fuzzing. These are applicableto various classes of software systems, and applying them to the softwarerunning on embedded systems is helpful as well. However, we explain thatthese techniques do not account for extended attack surfaces embedded de-vices have (see Chapter 1.4). Hence, there is a need for security analysisapproaches customized for embedded devices, to complement the aforemen-tioned techniques.We do not review techniques for network security, web security, andcryptography techniques. Network security techniques include, but are notlimited to, network policy controls, traffic encryption, and DDoS attacktraffic mitigation. These are applied to network infrastructure and mayprovide a layer of defense for embedded systems. However, in this thesis,we are considering defense measures inside the network perimeter and onthe host. Therefore, we do not cover the existing research work related tonetwork security. Web security techniques address attacks such as phishing,cross-site forgery, and cross-site scripting. These attacks target users ofgeneral purpose computers and therefore, do not directly affect embeddeddevices. Cryptography techniques have a wide range of applications and are102.1. Intrusion detection systemsused in both network-based and host-based security measures to protect dataconfidentiality. In this thesis however, we are not considering an adversaryviolating data confidentiality and therefore, do not review the correspondingliterature.2.1 Intrusion detection systemsIntrusion is defined as a set of actions that bypass the security mechanismsof a computer system [70]. This occurs when an adversary tampers withthe system via exploiting a vulnerability in hardware/software stack of thesystem. Intrusion detection is the process of monitoring the system andnetwork for any access, activity, and modification of code, data, hardware.An intrusion detection system (IDS) is a software or hardware componentthat automatically performs such monitoring process.IDSes are either host-based or network-based. Host-based IDS is in-stalled on the system and monitors operations of applications, communica-tion between applications, and applications and OS. Network-based IDS isattached to network. It monitors all the incoming and outgoing traffic onthe network and protects all the machines present on that network segment.Whether an IDS is network-based or host-based, it performs attack de-tection using signature-based, anomaly-based, or specification-based tech-niques [53, 70].In signature-based approach, intrusion is detected based on a predefinedmodel of attacks, e.g., sequence of events and sizes of specific packets in theattack. The advantage of signature-based systems is that they do not needto model the system they are monitoring. This reduces the complexity ofbuilding the IDS. The disadvantage of signature-based technique is that it isnot effective in detecting new attacks, and needs to be constantly updated.In anomaly-based approach the developer models the system using profilingand statistical techniques. This approach is suitable for detecting new at-tacks, however, it may have a high false alarm rate. False alarm occurs whenthere is no attack, but the intrusion detection system reports one. Speci-fication based approach is based on specifying the behavior of the system,112.1. Intrusion detection systemsaccording to its design and implementation. Violation from this specifica-tion is a sign of intrusion. This technique is also suitable for detecting newattacks. However, this approach may lead to a complex model that requireslarge memory.Techniques for building IDS include broad categories. Here we discusstheir limitations in addressing the constraints of embedded devices.Hardware-based solutions: Hardware-based techniques rely on spe-cialized hardware components that measure execution time, keep secret keys,etc. Timing Trace Module (TTM) and Trusted Platform Module (TPM)are examples of such hardware components [63, 74]. While using customhardware is efficient in terms of performance, it is not suitable for low-costembedded devices that are deployed on large scale as they result in addedper-device cost and an increase in update costs [51].AI-based solutions: There are many papers on building IDSes usingHidden Markov Models, Neural Networks, and Support Vector Machines.Warrender et. al. [84], Hu et. al. [43], and Hoang et. al. [41], use HiddenMarkov Models to design the decision engine of IDSes. Neural Networkshave been used to classify intrusions and detecting them [64]. Support Vec-tor Machines [44] have also been used to model the correct behavior of thesoftware so that deviation from the normal behavior is detected [82]. Sta-tistical techniques have also been used to detect abnormal behavior of thesoftware by analyzing large volume of audit data [86]. AI-based techniquesare suitable for modeling the behavior of large and complex software anddetecting unknown attacks. However, their false positives make them a poorfit for embedded devices. Many embedded devices are not directly interact-ing with users and hence, false alarms cannot be handled by individual users.In this case, even a small false positive rate of 0.5% can aggregate quicklyto an overwhelming 5000 false alarms for 1000 units running 10 applicationseach.Static analysis-based solutions: Static analysis techniques build amodel of the software based on the source code. These models are conserva-tive representations of the software and consequently, have no false positives.Wagner et. al. [83] propose a technique to build a model of the software122.1. Intrusion detection systemsbased on the system call-graph. They show that the call-graph techniqueresults in a high false negative rate, and they improve their technique by in-troducing non-deterministic pushdown automaton (NDPDA). In NDPDA,they build an extensive model of the software based on the system calls.However, this technique results in a high memory overhead. Giffin et. al.[36] propose the Dyck model to build an IDS based on static analysis of thesoftware and its system calls. In their work, they added context sensitivityto the model, removing some of the false negative inaccuracy that exists inthe static analysis techniques. While this improves the accuracy, it resultsin increasing the size of the model considerably. This is a huge disadvantagefor embedded devices with small memory capacity.Techniques developed for embedded devices: There are IDSesdeveloped for embedded devices using the techniques discussed above [16,63]. However, these IDSes are either designed for the communication link, orassume the presence of very specific architecture or hardware modules. Forexample, Mohan et. al. [63] propose an IDS for embedded systems equippedwith multicore processes running on a Hypervisor. A secure core is dedicatedto running the IDS which monitors the controller that is running on theother core. This work can be applied only to select embedded devices as thesystem must be equipped with a multicore processor as well as a TimingTrace Module (TTM). Also, it is designed only for higher end embeddeddevices that have enough resources to run a hypervisor. Berthier et. al.[15, 16], provide guidelines to build IDSes for smart meters. They propose aspecification-based IDS for network communications of smart meters. Thiswork is focused on building a network-based IDS and does not protect thehost if the attacks are not detected by the network-based IDS. Closse et. al.propose a tool for verification of real-time behavior of embedded systems[25]. However, they do not consider security properties in their work, nordo they discuss means to address memory limitations of embedded devices.Remote attestation: Remote attestation techniques [22, 55, 75] usea remote server to verify the security of a system. Information from thesystem is periodically sent to the server and is processed remotely. However,using this technique for run-time verification results in high communication132.2. Security analysisoverhead which increases energy consumption. This is a limiting factorfor many classes of embedded devices. It also requires the devices to beconnected to the remote server at all times. These limitations make thistechnique unsuitable for embedded devices that are deployed on a largescale in bandwidth and energy constraint environments.Runtime verification: A class of papers are dedicated to monitor-ing and analyzing the system during run-time [11, 38, 57, 58] for safetyproperties. Basin et. al. [11] and Gunadi et. al. [38] propose a newspecification language based on temporal logic for defining and monitoringsafety and security policies. Maggi et. al. [57, 58] propose an LTL-basedrun-time monitoring of business processes to verify their compliance withcertain constraints. Unlike us, they do not offer any mechanism for opti-mizing coverage for security invariants of the system within the memoryconstraints of embedded devices.2.2 Security analysisIn this section, we discuss different classes of existing techniques that areused to analyze security, fault-tolerance, or correctness of computer systems.Attack patterns: Attack patterns capture the common methods forexploiting system vulnerabilities. Each attack pattern encapsulates informa-tion including attack prerequisites, targeted vulnerabilities, attacker goals,and resources required. Thonnar et. al. [80] study a large dataset of networkattacks to find the common properties of some attacks. They develop a clus-tering tool and apply them on different feature vectors characterizing theattacks. Gegick et. al. [35] encode attacks in the attack database and usethem in the design phase to identify potential vulnerabilities in the designcomponents. Fernandez et. al. [33] study the steps taken to perform a setof attacks and abstract the steps into attack patterns. They study Denialof Service (DoS) attacks on VoIP networks and show that their patternscan improve the security of the system at design time, and help securityinvestigators trace the attacks.Although integrating attack patterns into the software development pro-142.2. Security analysiscess improves the security of the software, it has two disadvantages. First,attack patterns are often at a high level of abstraction, and require signifi-cant manual effort to apply. Second, for new embedded systems, there is nowell-known attack vector from which we can develop attack patterns.Attack trees: Attack trees are top-down hierarchical structures inwhich lower level activities combine to achieve the higher-level goals. Thefinal goal of the attacker is presented at the root. Byres et. al. [18] de-velop attack trees for power system control networks. They evaluate thevulnerability of the system and provide counter measures for improvements.McLaughlin et. al. [60] use attack trees for penetration testing of smart me-ters. Morais et. al. [65] use attack tree models to describe known attacks,and based on the trees develop fault injectors to test the attacks against thesystem. They test their analysis technique on a mobile security protocol.Attack trees are mainly designed to analyze predefined attack goals.However, many security attacks are not targeted and are based on the vul-nerabilities that the attackers opportunistically find in the system whiletesting it.Attack graphs: Attack graphs have been mainly used to analyzeattacks against networked systems. They take the vulnerability informationof each host in a network of hosts, along with the network information,and generate the attack graph. Sheyner et. al. [76] and Jha et. al. [49]propose techniques for automatically generating and analyzing attack graphsfor networks. They assume that the vulnerability information for each nodeis available. Based on this information, they analyze the chains of attacksand their effects in the network.To use attack graphs, the programmer needs the complete set of knownvulnerabilities on the host. If the hosts have unknown vulnerabilities, theanalysis will be incomplete.Attack Database: Databases such as National Vulnerability Database(NVD) [66] can be used to find attacks on general-purpose computer sys-tems. However, these databases are not easily transferable to various em-bedded devices. The reason is that these devices, unlike general purposecomputers, have very different hardware/software stack. For example, many152.2. Security analysisembedded devices are equipped with Application Specific Processors (ASP).This results in customized OS and software stack. Hence, an attack discov-ered against a common Linux kernel for x86 architecture may be applicableto many general-purpose servers, but applicable to a very limited number ofembedded devices. Another shortcoming of using existing attack databasesis that they cannot cover new attacks against embedded devices.Fault injection: Fault injection techniques have been used to evaluatefault tolerance of computer systems [9, 20, 78] In software implemented faultinjection (SWIFI), hardware faults are emulated by software. Tseng et. al.[81] used software-based fault injection to evaluation both security and errorresiliency of SCADA systems in power grids. The main limitation of faultinjection is that the state space of fault injection may grow exponentially.Also, not all the faults injected in the system have security-related impact.Detecting such faults, as the space of fault injection grows, is challenging.This limits the scalability and accuracy of fault injection for evaluating se-curity.Fuzzing: Fuzzing involves inserting random inputs to a program andevaluating their effects [61]. This process facilitates automated penetrationtesting. Some tools built based on fuzzing techniques include HP WebIn-spect [42], the IBM AppScan [45], and Acunetix web application securityscanner [8]. Neves et. al. presented a tool called AJECT for fuzzing theinput to the servers, based on predefined attack patterns [67]. Fuzzing mayuncover many of the existing bugs in the system. However, the effects offuzzing may not necessarily be security-related. Therefore, these tools re-port a high percentage of false positives [68]. Also, fuzzing techniques onlyfocus on feeding inputs to the programs. Therefore, they are most effectivefor systems that have well-defined communication protocols and architecture(such as web applications). Embedded devices are exposed to range of ac-cesses (e.g., physical access) and attacker actions (e.g., physically rebootingthe device) that may not easily be simulated by fuzzing techniques.162.3. Summary2.3 SummaryHost-based IDSes are widely deployed in general purpose computer systemsto protect them from attacks. They are useful as network-based IDSes mayhave false negatives and let the attackers exploit vulnerabilities of the host.Based on the critical nature of the applications of embedded devices, build-ing host-based IDSes for these systems is a necessity. However, embeddeddevices have characteristics that make building host-based IDSes for themchallenging. Due to these constraints, existing techniques for building host-based IDSes for general computers are not suitable for embedded devices.Furthermore, host-based IDS does not guarantee that an attack may notreach the software of an embedded system. Hence, analyzing security of theembedded system’s software is another important step to provide in-depthhost-based security. Prior work for analysis of security of computer systemsagainst attacks may be used with known attacks and vulnerabilities such asNational Vulnerability Database (NVD) [66] and Common Vulnerabilitiesand Exposures Database (CVE) [26]. With these techniques, the securityanalyst builds a model of specific attacks, and analyzes the steps required toapply them. However, as explained in Chapter 1.4, embedded devices haveextended attack surface that goes beyond general purpose machines, e.g.,servers. This makes developing security analysis techniques customized forembedded system, and complementing existing approaches, necessary.17Chapter 3Low-memory IntrusionDetection System forEmbedded SystemsIn this chapter we describe building a low-memory intrusion detection sys-tem for a class of embedded systems, namely smart meters. This chapteraddresses research question RQ1.1 from Chapter 1.5: How can we reduce re-source requirements of a host-based intrusion detection system for embeddedsystems? In this chapter, we study the effect of selective monitoring of anembedded device on both memory requirements and coverage provided. Weuse smart meters as a testbed for our IDS. We first describe our techniquefor building low-memory IDS and later, present the results.3.1 ApproachIn this section, we introduce our IDS for smart meters and explain howwe address the constraints discussed in Sec. 1.2 in our design. As in otherIDSes [31, 36, 41, 83, 84], we use system calls as the input to the IDS. Thisallows the IDS to access raw data of the interaction between programs andthe operating system.The IDS is based on a high-level model of the software running on themeter. Based on the model, we identify the events that represent the core be-havior of the software, and therefore, are important from the security pointof view. Our IDS selectively monitors the system calls based on the model,thereby detecting the important attacks, while satisfying the constraints of183.1. Approachsmart meters in terms of the computation and memory overhead.Building a model for general purpose computers’ operations may be in-feasible given their vast state space of operations. However, unlike generalpurpose computers, smart meters are designed to carry out a specific set ofoperations. As a result, it is possible to model the activities of the smartmetering software based on its architecture and use cases. Further, thereare standard specifications available for smart meters, for example [28]. Weuse an abstract model derived from such specifications.Based on the abstract model, we build a concrete model of our specificsmart meter. The concrete model of the meter captures all the proceduresimplemented for that specific meter and the control flow between them. Tobuild the concrete model of a specific instance of a meter, we map the ab-stract model to the implementation of the meter, using programmer definedtags/annotations. Different procedures in the code are mapped to the cor-responding components in the abstract model and the result represents thedetailed activities performed by the specific smart meter.We traverse the abstract model and for each component, identify theclass of attacks that could target its activities (such as storing data, networkcommunications, etc.). From the set S, which contains all system calls in thesoftware, we create a subset P of system calls that represent the vulnerableactivities. Through a procedure that we explain later, we assign a subsetof system calls in P to blocks of the concrete model and generate a statemachine of system calls that constitute the signature for the IDS. The IDSmonitors the executed system calls, verifies them with the state machineand detects any deviation from the state machine model, as an attack.This model-based approach of selecting system calls and building thestate machine enables us to monitor the entire state of the software (repre-sented by the concrete model), while considering only the important systemcalls that are involved in the potential attacks against the meter. This iscrucial to the feasibility of IDS designed for smart meters without compro-mising on the constraints.We discuss each of the above steps in more detail below.193.1. Approach3.1.1 Abstract and concrete modelsWe use technical specifications of the meter such as [28], to extract and ab-stract model of its operations. These specifications are long (over 100 pages)and in general language. The two important operations of the abstractmodel are consumption calculation and communication with the server.Consumption calculation includes initialization of the sensors, reading con-sumption data from the sensors, calculating consumption information, andpassing this information to the processes in charge of communicating withthe server.Server communication includes checking network connectivity, receiv-ing commands from the server, storing consumption information on physi-cal storage, retrieving data from physical storage and sending them to theserver, via the network interface.In the abstract model, we create blocks for each of the components ofthe meter. Each block, e.g., sensor initialization, contains the activities itentails to achieve its goal. Therefore, we represent the abstract model as anactivity diagram of the meter.We specialize the abstract model for specific instances of the meter soft-ware. This is called the concrete model.To build the concrete model of themeter, we map each block in the abstract model to the corresponding func-tions in the meter software that implement the functionality of that block,in an automated fashion as we show below. Figure 3.1 shows a portion of theconcrete model for two blocks of the abstract model. This concrete model isfor the SEGMeter, our open source smart meter from Smart Energy Groups[77]. In block 6, powerOutputHandler saves consumption information suchas power, energy, and energy channel, into a buffer. sendMessage passes thisinformation through serial communication to ser2net, which is a specializedprocess to pass data between procedures of SEGMeter. In block 7, getDatareceives information from ser2net, validateMessage verifies formatting of themessage, and readMessage processes the content of the message. Thus, theconcrete model may have multiple procedures for each block of the abstractmodel.203.1. ApproachTo automate the process of creating a concrete model of a specific smartmeter, we need semantic information provided by the developer. The devel-oper of the smart meter software needs to add tags to the procedures in thecode as per their functionality. We use these tags to automatically generatethe concrete model. We design our tagging system so that it satisfies twomain goals:1. Ease of use: The process must be straightforward for the developer sothat it is conveniently integrated with the design process.2. Flexibility: The process of concrete model generation must be flexibleto be applied to different implementations of the smart meter.To achieve the above goals, we design a hierarchical tagging system,that lets the developer express the intended functionality of a procedure interms of an n-tuple of common operations performed by the meter. Becausesmart meters typically perform a small set of operations, it is possible toassign unique labels for each of these activities, and map the proceduresto the activities. The activities are represented by the tags. By using thetags, the developer does not need to directly map the procedures to theblocks of the abstract model. The hierarchical structure helps the developerdo the process step by step and to refine the state space iteratively. Thissystem also provides the flexibility to generate the concrete model for a widerange of different implementations, as one procedure may have multiple tagsassociated with it.The code developer adds the tags as comments at the beginning of eachprocedure. Our custom model generator parses the code and based on theassigned tags, places the procedures in appropriate blocks. Further, themodel generator creates the call graph of the procedures based on which thecontrol flow between the blocks of the concrete model is determined. There-fore, the concrete model is represented as a function-level control flow graphof the system, where each function is tagged with the id of the correspondingabstract model block it belongs to.213.1. Approachser2netgetData()6Ͳ Passingdatatobesenttotheserver7Ͳ ReceivingconsumptiondatapowerOutputHandler()sendMessage()validateMessage()readMessage()Figure 3.1: Concrete model for portion of the abstract model3.1.2 System call selection and state machine generationThe abstract model and concrete model of smart meter together identifythe system calls that are likely to be involved in attacks, and hence must bemonitored. To identify the key system calls that are likely to be involvedin security attacks, we first traverse the abstract model step by step andaccording to the functionality of each block, find if there are attacks thattarget those functionalities. This process is done manually, but using awell-defined algorithm as we explain below.Our goal is to find P , the set of system calls to be monitored. We use theclassification proposed by Hansman et al. [40] to find the attacks that corre-spond to each block. Examples of attacks classes include spoofing, sniffing,etc. We assume S to be the set of all system calls generated by the smartmeter software. For each functionality targeted by an attack in the classifi-cation, we add the system calls in S that represent those functionalities tothe set P . For instance, there is a message passing step (for passing con-223.1. Approachsumption data) between blocks 6 and 7 in the abstract model (Figure 3.1).The message passing procedure is vulnerable to a man-in-the-middle attackand data spoofing. The system calls representing message passing includeconnect, send, and recv. Therefore, we add these system calls to the set P .Once we find the priority set P , we need to construct the state machinefor the system calls in P . We follow the procedure below.1. For each block of the concrete model, identify all the system calls inP that are associated with that block.2. From the system calls associated with each block, select the ones relat-ing to the specific functionalities of that block (for instance, connectand socket system calls for server communication blocks, read andwrite system calls for storage blocks, etc.).3. Until all the blocks of concrete model are covered do:(a) Pick an unmarked system call s that appears in the maximumnumber of the blocks of the concrete model. This results in reduc-ing the size of P while providing high coverage across all blocksof the concrete model.(b) Mark system call s.4. Output all the marked system calls.After assigning the system calls to the blocks of the concrete model, webuild a state machine that represents the concrete model of the smart meter.Figure 3.2 shows a small section of the concrete model where the con-sumption data is received from the sensors through serial communicationand stored in the physical storage. Three procedures of the code, namelycheckTime(), serialHandler(), and updateNodeList() are represented by threesystem calls: time, socket, and write. The procedures are executed one af-ter another and serialHandler() executes in a loop. Therefore, the regularexpression corresponding to these blocks will be time socket* write. Af-ter identifying the system calls corresponding to the blocks of the concrete233.1. ApproachTimesyncCheck_time()SerialCommunicationserial_handler()PhysicalstorageUpdate_node_list()time socket writeFigure 3.2: The state machine based on the concrete model: here the se-quence time socket* write represents the flow of this small section of theconcrete model.model using the procedure above, we build the expression through back-ward traversal of the concrete model and extraction of the patterns thatcorrespond to the paths.3.1.3 DiscussionIn this section, we discuss how our IDS addresses the constraints outlinedin Chapter 1.2.1. Performance: To build an efficient IDS, we have to be able to selecta subset of system calls that are representative of the behavior ofthe software. Our technique enables us to select limited system callsthat efficiently cover the important components of the concrete modelregarding the potential attacks against the smart meter. In Section 3.2,we show the overhead benefits of having a compact model for smart243.1. Approachmeters that are memory-constrained devices.2. No false positives: The concrete model of the smart meter is builtbased on sound static analysis of the code for a specific model of themeter. A static analysis technique may either be sound, or complete.A sound static analysis over-approximates the behavior of the pro-gram. On the other hand, a complete static analysis technique under-approximates the behavior of program. Bug finding tools designedbased on sound static analysis, cover all the valid execution paths ofcode. However, they may also consider certain execution paths thatare not feasible during run-time (e.g., due to certain restrictions onthe input which information is not available statically in the code).Exploring these extra paths, may result in detecting bugs that do notoccur during run-time and hence, producing false positives in findingbugs. In our IDS, false positive happens when valid execution of soft-ware is not included in the control flow graph of software. On theother hand, false negative happens when an invalid execution of soft-ware is included in the control flow graph. Therefore, using a soundstatic analysis, a false positive in bug finding tools (i.e., invalid pathin the control flow graph) corresponds to a false negative for our IDS.However, since the static analysis produces an over-approximation forthe paths of code and includes all possible valid paths, our IDS willnot have false positives.3. Software modification: The only modification we make to the code isthe addition of tags to the procedures to automatically generate theconcrete model of the software. It is important to note that the tagsare treated as comments in the code, and are read only by our modelgenerator. Hence, they do not affect the execution of the code or itsperformance.4. Low cost: Our technique is designed to build a model of softwarerunning on the smart meter that covers all the key components of thesoftware but at the same time has a small size, and therefore, fits in253.2. Evaluationthe meter’s memory. This means that it can be deployed on existingsmart meters, without any new components.5. Coverage of unknown attacks: Discussed in Section 3.2.Generalizability: The abstract model represents the main functional-ities of the meters that are common among different instances of meters.These functionalities are defined in standard documents released by gov-ernment departments in charge of deploying smart meters [2, 3]. As smartmeters in each region must comply with these standards, we believe thatthe procedure of applying the abstract model to smart meters and designingthe IDS, can be generalized to meters from different vendors.3.2 Evaluation3.2.1 Experimental setupWe implement our solution for the SEGMeter, an open source smart meterfrom smart energy groups [77] (Fig. 3.3). SEGMeter consists of two mainboards: 1) an Arduino board [12] with ATMEGA32x series microcontrollerwhich is connected to a set of sensors, receives sensor data, and calculatesconsumption information and, 2) a gateway board with Broadcom BCM3302V2.9 240MHz CPU and 16 MB RAM. The gateway board has LAN andWiFi network interfaces, and communicates with the utility server. It runsOpenWrt, which is a Linux distribution for embedded devices. OpenWrtallows the system developer to customize the device according to the limitedresources.The meter software consists of about four thousand lines of code and itis written in C++ and the Lua language. The C++ code resides on theArduino board and the Lua code resides on the gateway board. The boardscommunicate with each other through a serial interface.Our IDS runs on the gateway board and has two major components. Thefirst component starts when the smart meter boots up and attaches straceto the process we are monitoring. strace intercepts every system call made263.2. EvaluationFigure 3.3: SEGMeter: our open source meter testbed. The board on theleft is the gateway board in charge of communicating with the server, andthe board on the right is the Arduino board that receives consumption datafrom the the process and logs it to a file. The second component of the IDS runsevery T seconds, reads the log file, compares it with the model, clears thelog, and raises an alarm if a mismatch occurs. We have set T = 10secondsin our experiments. For SEGMeter, our IDS is built based on 29% of totalsystem calls. Examples of the system calls selected in our IDS include:open, write, recv, send, connect, read, close, ioctl. Other system calls suchas utime, fstat, chdir, newselect, pause, time, gettimeofday, etc. were notselected through our process explained in Sec. 3.1. We manually added thetags required to generate the concrete model of the meter (Sec. 3.1). Theentire process took about 6 hours.In our experiments, we first measure the performance overhead of ourIDS under memory constraints that are typical for smart meters. We com-pare the performance of our IDS to existing techniques that use the fullsystem call trace of the software to monitor its operation. We call this IDSthe full trace IDS. Then we evaluate the detection performance of our tech-nique for both unknown and known attacks. Finally, we discuss the effectof detection latency, T , on the performance of our IDS.273.2. Evaluation3.2.2 ResultsPerformance overhead: As stated earlier, an IDS developed for smartmeters should be able to operate under severe memory constraints, and stillachieve reasonable overheads. The SEGMeter has a total of 12MB RAMavailable. To study the effect of memory constraints, we added dummyprocesses to take up memory with no processing overhead. We run ourmodel-based IDS and the full-trace IDS under these constraints.We measure the performance overhead as the ratio of the time taken toread the system call log, analyze it, and compare it against the model, tothe time taken by the smart meter software to produce the trace. Note thatwe do not perturb the software in any way except to run strace on it, whichhas minimal overhead (less than 1%). Table 3.1 shows the results.As can be observed from the table, the performance overhead for the full-trace IDS is considerably higher than that incurred by our IDS. Even whenthe entire memory of the SEGMeter is available to the IDS, the overhead forthe full-trace IDS is over 100%, while our IDS has only 4% overhead. Thismeans that for 10 second logs, the full-trace IDS takes more than 10 secondsto perform detection and hence, falls behind the software. Further, increas-ing the time between analyzing the logs does not help with the overhead offull-trace IDS as the size of the log will also increase (we have verified thisfor 10, 20, 30 second logs).The main reason for poor performance of the full-trace IDS is that itsignificantly increases the size of the model compared to our IDS, and hencecauses thrashing i.e. page faults due to the working set size not fitting inmemory. This can be confirmed by the fact that the overhead of the full-trace IDS increases as the memory available decreases from 12 MB to 6 MB.Considering the long lifetime of smart meters (over 15 years), this overheadcan be a major problem, as memory requirements may change substantiallyin this time frame. On the other hand, the performance overhead of ourIDS remains constant as the memory capacity is decreased, even down to 6MB.Unknown attacks: As stated in the threat model, the goal of the at-283.2. Evaluation12 MB 9 MB 6 MBFull-trace IDS (10s) 165.2% 214.6% 315.1%Model-based IDS (10s) 4.0% 4.0% 4.0%Table 3.1: Running time overhead of our model-based technique andcomplete-system-calls technique.tacker is to change the behavior of the software in a way that is stealthyand not easily detectable. To do this, the attacker needs to intercept theprogram when it is running and inject code to change the flow of execu-tion (e.g., through a buffer overflow attack). Therefore, to mimic unknownattacks, we developed a code injection procedure that works as follows.For each injection, a random procedure of the software containing systemcalls is selected and a few (1 to 8) lines of code are copied and pasted inthe same procedure. Only one injection is performed per run to increasethe stealthiness of the attack. While the attacks generated may not achievethe attacker’s desired goals, they serve as a means to evaluate the detectioncapability of our model against stealthy attacks that change the executionof the code. The attacks generated using the above technique are difficult todetect because (1) we do not introduce new system calls that would triggerIDSes that look for system calls outside the allowed set, and (2) the copy-pasted code belongs to the original software and would hence be missed byIDSes that do not consider the system call ordering in their signatures.To perform the injections, we divided the components of the software intothree categories: 1) server communication: the functions that communicatewith the utility server, 2) storage and retrieval: the functions that processconsumption data, back it up, read it from flash memory, etc., and 3) serialcommunication: the functions that receive and process consumption datathrough serial communication interface from procedures in charge of con-sumption calculation. Using the above procedure, we created 50 injectionsin each category, adding up to a total of 150 injections.In addition to the full-trace IDS introduced earlier, we compare ourIDS with two other IDSes, namely (1) random, and (2) most-popular. Inthe random IDS, we picked the system calls to monitor randomly from the293.2. EvaluationComponent Random (%) Popular system calls Full trace (%) Model-based (%)Minimum Average MaximumServer communication 32 36 92 59 62 63Storage & retrieval 14 44 84 73 74 78Serial communication 42 28 88 67 72 74Total 29.3 36.0 88.0 67.4 69.6 71.7Table 3.2: Code injection detection coverage of our technique Versus othertechniques for each sub-system of the meterset of all the system calls in the software. In the most-popular IDS, wepicked the system calls that have the highest frequency in the code. Theexpectation is that the higher the frequency of a system call, the bettercoverage it potentially provides. In both cases, we chose the same numberof system calls to monitor as our model-based IDS, for fairness.The detection results are shown in Table 3.2. The random IDS providesan average coverage of 29.3%, and the most-popular IDS provides an averagecoverage of 36%. Our IDS provides an average coverage of 69.6%, while thefull-trace IDS provides an average coverage of 88%. The reason that the full-trace IDS does not provide 100% coverage is that many of the procedurescontain loops, and mutating the lines within a loop does not change thesystem call sequences.When building the model-based IDS according to the steps provided inSec. 3.1.1, it is possible that we have more than one option for assigningsystem calls to blocks of the concrete model to build the IDS. To studythe effect of these options, we study the maximum and minimum coverageprovided by the different sets of system calls chosen by our IDS. Note thatthe maximum/average/minimum results are calculated for each componentby considering all possible combinations of the system calls chosen by ourIDS for that component. As the table shows, the difference between themaximum and minimum values of total coverage is 4.3%. This shows thatthe effect of different combinations on the coverage of the IDS is negligible,as long as it is based on the procedures provided in Sec. 3.1.1.Known attacks: To evaluate our IDS against real attacks on smartmeters, we implemented four attacks for the SEGMeter. To our knowledge,there is no publicly available dataset of attacks for smart meters at the303.2. Evaluationsystem call granularity that we can use for our evaluation.The goal of the attacks is to help the attacker gain financial benefitsfrom tampering with the meter software through changing the consumptiondata, etc. Further, we verified that none of these four attacks are detectedby server side defenses or other techniques developed on the meter. Webriefly explain the attacks below:1. Communication interface attack: The goal of this attack is to modifyconsumption data sent to the server. ser2net is a component of SEGMeterthat receives consumption data from the Arduino board and passes it to thegateway board (Figure 3.1). We injected code to change the informationflow from ser2net and modify the data before it is sent.2. Physical memory attack: The SEGeter writes data to flash memorywhenever the network is not available. We injected code to temporarilydisable the network so that data is written to flash memory. This providesthe opportunity for the attacker to modify data on the flash memory sowhen the data is retrieved, false data is sent to the server.3. Buffer full attack: We changed the control flow of the communica-tion between the gateway board and controller board to send fake 128 bytemessages with a frequency of 30 times per second. This causes the receiverbuffer on the controller board to always be full. Therefore, any legitimatecommand sent from the server will not be processed, including disconnectionrequests.4. Data omission attack: We inject code that connects to the port2000, which is the port through which the gateway board and the Arduinoboard communicate and exchange consumption data. The timeout for thecommunication is 10 seconds. Our attack code periodically (after the 10-second timeout) connects to port 2000 and reads available consumptiondata. This data will be deleted by the controller board after it is read.Therefore, when the legitimate connection is established again, this data isnot available to be sent to the server, and hence the server records lowerconsumption data than the legitimate consumption.Our IDS was able to successfully detect all four attacks above. As ex-plained in Sec. 3.1, we follow a comprehensive attack classification to identify313.3. Summarysecurity critical system calls for blocks of our model. All the attacks we con-sidered use one or more system calls that we identify as security critical inSec. 3.1. Hence, our IDS successfully detects all the attacks. This reiter-ates the value of using model-based techniques to choose the system calls tomonitor in the IDS.Detection latency: As mentioned before, our IDS reads the generatedsystem calls every T seconds and compares it with the model. Therefore, thevalue of T determines the maximum delay for detecting attacks. However,a smaller T results in higher performance overhead, as it is more intrusive.Fig. 3.4 shows the variation of the performance overhead incurred byour IDS versus parameter T . We observe that at T = 10s, the performanceoverhead drops to 4.15%, and we choose this value as the timeout T . Webelieve this delay is a reasonable trade-off between latency and overhead.Note that even with a delay of 1 second, our performance overhead is only16%, which is 10x less than the overhead of the full-trace IDS (at 160%).This is the average performance overhead among different model-based ID-Ses that can be built. But the performance does not change significantlybetween different model-based IDSes (less than 2%) as the size of the modelis the same for all of them.3.3 SummaryIn this chapter, we designed a model-based IDS that satisfies the constraintsof embedded systems. We showed that our IDS incurs low performanceoverhead on our smart meter while providing reasonable detection coveragefor both known and unknown attacks. In the next chapter, we generalize ourtechnique to build an optimized IDS with respect to user-defined criteria.323.3. Summary0 20 40 60 80 10005101520Delay time (s)Overhead(%)Figure 3.4: CPU overhead for different monitoring time values (T ).33Chapter 4Optimizing IntrusionDetection System forEmbedded SystemsIn this chapter, we extend our approach discussed in Chapter 3 and lay outthe problem of building an IDS for memory-constrained embedded systemsas an optimization problem. This chapter addresses RQ1.2 from Chapter1.5: How can we optimize a host-based Intrusion Detection System for em-bedded system, with respect to available memory?In this chapter, we propose a technique that given the security invariantsof the system, automatically builds an IDS that maximizes coverage of theinvariants within the available memory. The coverage function in our tech-nique is flexible and can be defined by the user. Therefore, our techniqueproduces a customized IDS for every device, with respect to its memorycapacity, and the security invariants provided by the user.4.1 ApproachIn this section, we explain our approach for building an IDS for embeddeddevices, for optimizing the coverage of the security properties of the systemwith respect to its memory constraints.We use examples from a smart metering platform to explain our solution.344.1. ApproachSendconsumptiondata SerialinterfaceReceiveconsumptiondataStoredataintoflashRetrievedatafromflashCommunicatewithserversensorsUtilityServerFigure 4.1: An execution path of smart meter operations used as a runningexample.݌ଵ ݌ଶ ݌ଷݒଵ ݒଶ ݒଷ ݒସ Invariants(V)SecurityProperties(P)ɒ࢖૚ɖࢂ૜Figure 4.2: Formulation of the IDS as an optimization problem.4.1.1 Problem formulationIn this section we formulate the problem of building an IDS as an optimiza-tion problem. Fig. 4.2 illustrates the formulation. We define the followingterms in the formulation:• We let Σ denote the set of all the system calls that may be executedby the software (on a given OS).• The set P = {p1, p2, ..., pm} is the set of security properties of the sys-tem. These properties define the integrity and availability propertiesof the system that should be preserved so that the system is secure.Examples of such properties are integrity of data storage/retrieval and354.1. Approachavailability of network communication.• τpi indicates the set of invariants that must hold, so that property piis verified. Each of the invariants in τpi is defined over system calls Σ.We explain the invariants in sec. 4.1.3.• The set V = ∪mi=1τpi = {v1, v2, ..., vn}, denotes all invariants in thesystem that must hold so that the correctness of all pi ∈ P is verified.• We define χvi = {pj ∈ P |vi ∈ τpj}. Intuitively, χvi denotes the set ofsecurity properties for which, verification of vi is a necessary condition.• D(V ′) indicates an IDS monitoring the set of invariants V ′ ⊆ V . TheIDS D is a state machine defined over Σ. We will explain how to buildthis state machine later. In this chapter, we assume that the IDS Dis a Bu¨chi automaton, and in Ch. 4.1.3 we will explain why we havemade this choice.• We denote the size of IDSD(V ′) by |D(V ′)| and define it as the numberof the states in the IDS. We let M denote the upper bound for thesize, determined by the memory constraints of the system.• U : 2V → IR is a coverage function defined over the subset of invari-ants, and assigns a real number value to each subset. Different subsetsof invariants may have a different value depending on their role inverifying the security properties. We assume that the coverage func-tion is monotonic. Formally, we define monotonicity as the following:∀x, y ⊂ V x ⊂ y ⇒ U(x) < U(y). The monotonicity assumption isreasonable as we expect to have improved coverage when making theset of monitored properties larger.Our goal is to build an IDS D with respect to assumptions above, andbased on the subset of invariants V ′ ⊆ V so that the 1) the size of theIDS is smaller than or equal to the available memory M , and 2) U(V ′) ismaximized. Formally, we define our goal as the following:364.1. Approach• We findD(V ′), V ′ ⊆ V and |D(V ′)| ≤M such that ∀V ′′ ⊆ V, |D(V ′′)| ≤M ⇒ U(V ′′) ≤ U(V ′).In our formulation, the user can define their own coverage function U .Later in this section, we introduce two coverage functions and explain theirrationale.4.1.2 System overviewWe briefly explain the high level steps that we take to build the IDS below:• Steps 1-2: The goal of the first two steps is to define the set of highlevel invariants that verify the security properties of the system. Wecall these abstract invariants. These invariants verify the availabilityand integrity properties of the system from the security perspective.We use Linear Temporal Logic (LTL) [29] to define these invariants.LTL is a logic to express temporal relations among the monitored en-tities at runtime. We extract abstract invariants from the SoftwareDesign Document (SDD) which presents the architecture, data, andfunctional specification of all the components of the system (see [46]).For instance, execution paths of the system, similar to what was shownin Fig. 4.1 are presented in the SDD. SDDs are often used as imple-mentation guidelines and for defining gray box and functional testcases [7, 13]. We define abstract invariants once for an entire class ofembedded devices, and if necessary, tailor them for different models ofan embedded device.• Steps 3-4: We convert the abstract invariants into concrete invariants.Concrete invariants capture the code-level behavior of the system. Toachieve this, we substitute the propositional variables of abstract in-variants, which are functions described in design document, with thecode-level functions that implement them. Later, through static analy-sis, we substitute these functions with the patterns of system calls thatare executed within the functions. Hence, in the concrete invariants,system calls of the code are used as the propositional variables.374.1. Approach• Step 5: After building the concrete invariants, we build a Bu¨chi au-tomaton [34], to monitor the concrete invariants. However, the statespace can be large (exponential in the worst case) and exceed the avail-able memory capacity of the device. Therefore, we select invariantsthat maximize the coverage (U) of security properties of the system.Many definitions for security coverage have been suggested [5, 69].Therefore, we designed our technique so that it is not bound to a sin-gle definition for the coverage, and we enable the user to define theirown coverage function. We also propose two approaches for definingthe coverage and build IDSes based on them. Our IDS checks thesystem calls’ execution at run-time with a Bu¨chi automaton. If thebehavior of the system deviates from the set of monitored invariants,it reports it as an intrusion that has been detected.4.1.3 DetailsIn this section, we provide the details on how to build the invariants forsecurity, and convert them into an IDS.InvariantsA system is secure, if it achieves and sustains its mission according to a se-curity policy. We model the security policy of the system by defining the setof invariants V that must be preserved during run time. These invariantsverify the fundamental security properties of availability and integrity [71]of the system. For example, integrity of consumption calculation, integrityof communication to server, availability of data storage/retrieval, and avail-ability of server communication are security properties of a smart meter.Breaking any of these properties may result in loss of data and/or incor-rect billing. Therefore, the user defines the invariants (set V ) that verifycorrectness of all the properties pi ∈ P .We use Linear Temporal Logic (LTL) to define the invariants V , verifyingproperties P . Temporal logic is a formalism for describing properties of asystem over time. LTL describes the properties of runs of a system, which384.1. Approachmakes it suitable for verifying the status of a system during run time. LTLintroduces the operators © (next), 2 (globally or always), 3 (eventuallyor in the future), and U (until) [85]. We use these operators to definethe invariants. We define the invariants in two levels. First, we definethem at a high level and call them abstract invariants. Then, we convertthem to detailed, implementation specific invariants and call them concreteinvariants.Abstract invariantsAbstract invariants capture the availability and integrity requirements of thesystem according to the software design document (SDD) [46]. This doc-ument presents the architecture, functional specification, and control flowof all the components of the system. We consider all the execution paths(from sequence diagrams for instance) that form a security property pi ∈ P ,and specify the invariants that should hold so that the path is correctly ex-ecuted. For instance, the operations depicted in Fig. 4.1 presents a portionof the procedural flow of the smart meter in its SDD. The electricity con-sumption data is received via sensors, passed through serial communicationinterface and then stored in the flash memory for backup purposes. Later thedata is retrieved from the flash memory and sent to the utility server. Thisoperation may be compromised at different stages by an attacker makingthe functions or the resources unavailable (e.g., killing the running process,changing the execution path through corrupt input). Therefore, we needinvariants to make sure that these operations are not compromised. UsingLTL, we formulate the invariants that address the availability and integrityproperties of the system as shown in Table 4.1.Concrete invariantsIn the next step, we convert the abstract invariants into concrete invariants.We substitute the functional descriptions in the abstract invariants withthe code-level functions. Later, using static analysis, we substitute thesefunctions with the automaton representing the system-call-based regular394.1. ApproachInvariant description Invariant formulation Targeted propertyv1: Consumption data received fromserial interface must eventually 2(receive consumption data⇒ p1: Availabilitybe stored in the flash memory 3store data into flash) of storage/retrievalv2: Data stored in the flash memory 2(store data into flash⇒ p2: Integrity of storage/retrievalmust eventually be retrieved 3retrieve data from flash) p1: Availability of storage/retrievalv3: Data retrieved from flash memory must 2(retrieve data from flash⇒ p3: Integrity of network communicationeventually be sent to the server 3communicate with server) p4: Availability of network communicationv4: Storing data on the flash ¬(¬store data into flash Umemory must be after data is (¬store data into flash∧ p2: Integrity ofreceived from serial interface ¬receive consumption data)) storage/retrievalv5: Retrieving data from ¬(¬retrieve data from flash Uflash memory must (¬retrieve data from flash∧ p2: Integrity ofbe after data is stored ¬store data into flash)) storage/retrievalon the flash memoryv6: Sending data to theutility server must ¬(¬communicate with server U p3: Integrity ofbe after the data is retrieved (¬communicate with server∧ network communicationfrom the flash memory ¬retrieve data from flash))Table 4.1: Abstract invariants for an execution path of smart meter.expressions that are executed within those functions.For example, Fig. 4.3 shows parts of serial talker function used in oursmart meter testbed. This function is written in the Lua language on oursmart meter platform, and implements receive consumption data part ofFig. 4.1. As the name suggests, serial talker listens to a specific port andthrough a serial interface, receives consumption data sent from the sensorcontroller. The automaton resulting from static analysis of this function isshown in Fig. 4.3 and is described as (sr∗c). Although LTL does not includethe star operation (as in regular languages), we can add these automatonconnectives to it [85], without changing its semantics.4.1.4 Building the modelHaving all the concrete invariants, the next step is to build a state ma-chine that verifies the invariants. Given that the invariants are presentedas LTL formulas, we build a Labeled Generalized Bu¨chi automaton = ={Q,Σ, δ, S, F} that has an accepting language equivalent of the invariants[34]. In this formulation, Q is the set of states of the automaton, Σ isthe alphabet of the input for the automaton, δ : Q → 2Q is the transitionfunction, S is the initial state and F is the set of designated states. Thisautomaton will be our IDS D(V ′), defined in Sec. 4.1.1. V ′ ⊆ V indicates404.1. Approachwhat subset of invariants we will use in building the automaton. A word ofinfinite length is accepted by the automaton = if it has a run that visits adesignated state infinitely often. The details of building a generalized Bu¨chiautomaton from an LTL formula are provided in Gastin et al. [34]. Eachstate of = contains labels indicating what sub-formulas of I are satisfied inthat state. At run-time, = detects violation of an invariant if it transitionsto a state which has no path to a designated state in F . Otherwise, it willnot detect a violation. This may lead to false negatives if the system tran-sitions to a state where a path to a designated state exists, while transitionto that state never occurs.The state space of the state machine monitoring all the invariants maybe exponential in the worst case. Considering the limited available memory,we may not be able to build a state machine that includes all the invariants.Therefore, given the upper bound M for the size of the IDS, we select theinvariants that maximize the coverage function U , as stated in sec. 4.1.1.The role of the coverage function is to quantify the coverage provided bythe selected invariants. Our solution is structured in a way that the usercan use their own coverage function in the formulation. Here, we define twometrics and build two coverage functions based on them.We base our IDSes on the metrics for security coverage suggested bythe Computer Security Division of National Institute of Standard and Tech-nology (NIST) [69], and Computer Emergency Response Team (CERT)’sguide on measuring software security in its annul research report [5]. Wecall these IDSes MaxMinCoverage IDS and MaxProperty IDS. We explainthem below.MaxMinCoverage IDSIn this approach, our goal is to maximize the minimum property coverageprovided for each of the security properties of the system. We calculateproperty coverage for each of the individual properties pi ∈ P based onthe portion of invariants verifying pi that are included in the set of selectedinvariants to build the IDS. We provide the formal definition of property414.1. Approachfunctionserial_talker(){…serial_client =socket.connect(gateway_add,port)…while(condition){…stream,status,partial=serial_client:receive(data_len)…}…serial_client:close()}1 32srcs:socket.connect()r:serial_client.receive()c:serial_client_close()Figure 4.3: We convert functionsinto automaton connectives throughstatic analysis and then into con-crete invariants. The labels on statetransitions correspond to the systemcalls executed in the code.ݒଵ ݒସ݌ଵ ݌ଶInvariantsSecurityProperties݌ସݒଶ ݒଷ ݒହ ݒ଺݌ଷFigure 4.4: The invariants v1 to v6verify the properties p1 to p4.coverage and the coverage function of the IDS for MaxMinCoverage IDS,and then explain it with an example.For IDS D(V ′), the property coverage of property pi ∈ P , is defined asthe percentage of the invariants in V verifying pi, that are included in V′(and hence, included in the IDS D(V ′)). Note that to fully cover a property,all invariants that are mapped to it need to be checked. Based on this,we denote property coverage of pi with respect to IDS D(V′) by piD(V ′)(pi)(expressed as percentage):piD(V ′)(pi) =|τpi ∩ V ′||τpi |× 100;The coverage function U is defined as the smallest property coverage pro-vided for any of the properties pi ∈ P . Formally, we denote the coveragefunction of IDS D(V ′) as:U(V ′) = min{piD(V ′)(pi)|pi ∈ P}.We explain the above formulation with an example. In Fig. 4.4, we showsix invariants v1 to v6, defined in Table 4.1, and the corresponding securityproperties for the smart meter. As shown in Fig. 4.4, invariants {v1, v2}verify availability of storage/retrieval (p1). Invariants {v2, v4, v5} verify in-tegrity of storage/retrieval (p2). Invariants {v3, v6} verify integrity of server424.1. Approachcommunication (p3). Finally, invariant v3 verifies availability of server com-munication (p4). Formally, we have τp1 = {v1, v2}, τp2 = {v2, v4, v5},τp3 = {v3, v6}, and τp4 = {v3}.In this example, we assume that we have the memory capacity to monitorno more than four invariants. The size of the generated IDS will depend onthe invariants’ structure, but in this example, we ignore this for simplicity.Selecting the invariant set {v1, v2, v3, v4} will result in property coverage of100% for p1, 66% for p2, 50% for p3 and 100% for p4. Hence, the coverageprovided by the IDS (as determined by the smallest property coverage) willbe 50%. We can easily verify that this is the best coverage we can obtain inthis example.The benefit of the coverage function used in this IDS is that it distributesthe coverage among all the security properties as opposed to monitoringonly some properties and leaving the others completely vulnerable. This isimportant if the user does not have any other resources to strengthen thesecurity of the unmonitored properties.MaxProperty IDSIn this IDS, our goal is to maximize the number of the properties that arecompletely verified by the IDS, as opposed to the MaxMinCoverage IDSthat tries to distribute the coverage among all the properties.We use the same definition for property coverage as we used for MaxMin-Coverage IDS. We denote property coverage of pi with respect to IDS D(V′)by piD(V ′)(pi):piD(V ′)(pi) =|τpi ∩ V ′||τpi |× 100Based on this, the coverage function U is the number of properties with theproperty coverage of 100%:U(V ′) = |{pi ∈ P |piD(V ′)(pi) = 100}|.We consider the example from previous section. Again, for simplicityin this example, we assume that we have the memory capacity to mon-434.1. Approachitor no more than four invariants. In Fig. 4.4, selecting all the invariants{v1, v2, v3, v4, v5, v6} will result in property coverage of 100% for all the prop-erties p1, p2, p3, and p4. By looking at Fig. 4.4, we notice that by selectinginvariants {v1, v2, v3, v6} we can have property coverage of 100% for prop-erties p1, p3, and p4. We can see that there are no other four invariants thatcan achieve property coverage of 100% for three properties. Based on this, ifwe only have capacity for monitoring four invariants, the set {v1, v2, v3, v6}gives us the best result in terms of the number of properties.The benefit of the coverage function used in this IDS is that knowingthat some properties are 100% covered, the user may be able to apply othertechniques (e.g., code hardening) on the uncovered components of the code.Building the IDSAlgorithm. 1 shows the process of selecting the invariants to build the Bu¨chiAutomaton. To build MaxMinCoverage IDS or MaxProperty IDS we needto pass their corresponding coverage function U (defined in Sec. 4.1.4 andSec. 4.1.4) to the algorithm. In general, the user may define their owncoverage function U and use it as an input to the algorithm.In lines 5 through 10 of the algorithm, we build a bipartite graph g. Onepart of the graph are the nodes representing the security properties, andthe other part of the graph are the nodes representing the invariants thatverify those properties. g[i][j] = 1 if and only if V [i] ∈ τp[j]. In line 12,we go through the subsets (represented by array S[]) of the invariants V[]in descending order of their size (the number of invariants they include).In line 13, we check if we have already calculated an automaton within theconstraint M , using a superset of S[i]. If so, we do not process S[i] as itwill not give us any better results. This is because we assume that thecoverage function is monotonic (see Sec. 4.1.1). In line 16, we pass the setof currently selected invariants (S[i]) to the function calculateBuchi. Thisfunction calculates the Bu¨chi automaton for the set of invariants we passit. The details of building a Bu¨chi automaton is in [34] and we do notdiscuss it here. If the size of Bu¨chi automaton does not exceed M (line444.1. ApproachALGORITHM 1: Algorithm for building the IDSData: V[] Invariants, P[] Security propertiesResult: A the IDS automaton1 invariantSet = ∅;2 bestUtility = 0;3 Graph g[][];4 bool mark[];5 for i = 1 to size of V do6 for j = 1 to size of P do7 if V[i] ∈ τp[j] then8 g[i][j] = 1;9 end10 end11 end12 for all S[i] ⊂ V, in the descending order do13 if for any j, S[i] ⊂ S[j] and mark[j] == true then14 continue;15 end16 A, mem = calculateBuchi(S[i]);17 if mem ≤ M then18 mark[i] = true;19 Graph h[][];20 for all pairs of j, k V[j] ∈ S[i] and pk ∈ χV [j] do21 h[j][k] = 1;22 end23 if bestUtility < U(g,h) then24 bestUtility = U(g,h);25 stateMachine = A;26 end27 end28 end29 return stateMachine;454.1. Approach17), we mark S[i] (line 18) to make sure that we do not process any ofits subsets in the future, as their result will not be better than S[i] (dueto the monotonicity of the coverage function). Then, we build the vertex-induced subgraph h of graph g (lines 20 through 22). Subgraph h representsthe invariants and properties monitored by the Bu¨chi automaton. We passboth the original graph g and the subgraph h to the coverage function Uin line 23. By comparing the original graph and the subgraph, function Ucalculates the coverage. We compare the result with the best coverage wehave calculated so far. Whenever we achieve a better coverage within thememory constraint, we update the Bu¨chi automaton (line 25). In the end,we return the Bu¨chi automaton that provides the best coverage whose sizedoes not exceed M (line 29).The worst case time complexity of this algorithm is exponential, withrespect to the number of the invariants and the sizes of the invariants. Thereason is that, in the worst case, we have to go through all the subsetsof invariants and build a Bu¨chi automaton based on them (which may beexponential with respect to the size of the invariants). However, to generatethe IDS, the algorithm is executed offline and only once. In our experiments,the size of the invariants is around 30. Therefore, the algorithm is not asignificant performance bottleneck.Algorithm 1, given calculateBuchi function, finds the set of invariantsthat form a Bu¨chi automaton with the highest coverage (as determined byfunction U) among all the set of invariants that form a Bu¨chi automaton(using calculateBuchi) that is smaller than or equal to size M .Proof. We consider two cases:Case 1, the condition in line 13 is never satisfied : In this case, thealgorithm examines all possible subsets of invariant set V , and picks thebest one in lines 23 through 26. Therefore, the algorithm finds the optimalanswer.Case 2, the condition in line 13 is satisfied : In this case, we prove bycontradiction that the algorithm finds the optimal answer. Hence, we assumethat the algorithm finds a sub-optimal answer, If the condition in line 13 is464.1. Approachtrue for some S[i] ⊂ V . This would be due to building state machine A inline 16, using subset Ssub ⊂ V , while the best state machine is the resultof using Sopt ⊂ V . This entails that Sopt is not examined by the algorithmin lines 16 through 26. Hence, Sopt satisfies the condition in line 13. Thiscondition implies that there exists S[j] ⊂ V where Sopt ⊂ S[j], and S[j] hasalready been examined by the algorithm, which is why mark[j] == true inline 13. We denote the bipartite graphs that may be calculated by formulain line 21 for Sopt and S[j], as hopt and hj respectively. We have:U(g, hopt) is optimal ⇒ U(g, hopt) ≥ U(g, hj)Since U is monotonic:U(g, hj) ≤ U(g, hopt)⇒ S[j] ⊆ SoptThis is a contradiction as we already know that Sopt ⊂ S[j].4.1.5 OptimizationsIn the previous section we assumed that the invariants are independent.This means that for any given i and j where i 6= j, monitoring invariant vidoes not provide any information regarding the state of invariant vj . How-ever, by studying the invariants of the system, we observe that monitoringcertain invariants may result in providing coverage for other invariants aswell. Therefore, we design an optimization pass that reduces the size of theset of invariants, while preserving the coverage that the original invariantsprovide. We explain this in Sec. 4.1.5. This helps avoid monitoring in-variants that overlap each other and therefore, make better use of system’slimited memory.In the previous section, we also assume that all invariants are equallyimportant from the security perspective. However, due to some data beingmore sensitive than others, fault tolerance mechanisms already in place, etc.,violation of some invariants may have a higher security impact compared toviolation of others. Therefore, in Sec. 25, we introduce an algorithm to474.1. Approachtake this into consideration and produce optimal IDS with respect to bothmemory constraints and importance of invariants relative to each other. Thisallows the user creating an IDS that automatically allocates more memoryto invariants that monitor more important components of the system, andtherefore provides higher coverage for those compared to other components.Invariant reductionBy studying the invariants of a system and the coverage provided by moni-toring them at run-time, we observe that we may substitute several invari-ants with one, and achieve comparable results. This is important as it willallows us to save memory. We explain this further with an example. In Ta-ble 4.1, invariants v1, v2, and v3 are verifying three steps of a functionalityof the system which states ”Consumption data received from serial inter-face must eventually be submitted to the server”. Formally, we show thisinvariant as the following:u : 2(receive consumption data⇒ communicate with server)We note that u is less complex than union of v1, v2, and v3. Therefore,its corresponding state machine would be smaller than the union of statemachines of all these invariants. While it is possible that either of v1, v2, orv3 are violated in spite of u holding true, we expect a deviation from normalexecution of software to propagate. Therefore, at run-time, violation of v1,v2, or v3 is likely to lead to violation of u as well. This makes u a goodapproximation for v1, v2, and v3 (see Ch. 4.2).The above example takes advantage of the fact that in certain situations,eventually () operator may define a transitive relation between states ofthe system. Based on this, we design an algorithm for reducing the spaceof invariants and present it in algorithm. 2. We explain this algorithm inmore details here. In line 1, we initialize the invariant set V ′ with the inputinvariant set. V ′, at the end of the algorithm, keeps the reduced set ofinvariants. A round of reduction consists of comparing each invariant in V ′with all the other ones, to find a pair that can form a transitive chain. This484.1. Approachsearch is shown in lines 3 and 4. We compare any pair of invariants in V ′together. If the pairs fit the criteria to be reduced (line 5), we reduce themto a new invariant vnew and add it to V′ (line 6). In line 7, we mark thatthe new invariant vnew covers both invariants vi and vj . It is easy to showthat if the size of the input set V is n, we need to perform at most n − 1reduction rounds until no further reduction is possible. The reason is thatthe maximum length of a transitive chain in the input set may be at mostn. Since in each round of reduction we are comparing all the invariantstogether, we will be reducing the length of the maximum chain by at least1. Therefore, after at most n−1 rounds, there will not be any new reductionpossible. After creating the new, compact invariants, we need to remove allthe old invariants that were used to create the new ones. Therefore, in lines13 through 19 we mark these invariant to be removed from the set, andfinally in lines 20 through 24, we remove them from V ′.The time complexity of this algorithm is determined by the three loopsin lines 2, 3, and 4. The length of each loop is at most |V |, which indicatesthe size of set V . Therefore, the time complexity of the algorithm is O(|V |3).Since we allocate constant number of two-dimensional arrays of size |V |2,the memory complexity of the algorithm is O(|V |2).Invariant rankingBy studying the invariants of the system that verify its correctness, weobserved that not all of them necessarily have the same importance. Forexample, we review the invariants listed in table 4.1. Invariant v1 statesthat consumption data must eventually be stored in a file. This is importantas data not stored in persistent memory may be lost due to a malicious userrebooting the system at a specific time, or activation of faults that maycrash the meter. Invariants v2 and v3 states that consumption data storedin a file must be eventually retrieved and finally be sent to the server. Theseare also essential properties for the meter to work correctly. Violation ofthese invariant is an indication that the meter is not following its normalbehavior to correctly submit consumption data to the server. However, from494.1. ApproachALGORITHM 2: Algorithm for invariant reduction.Data: V InvariantsResult: V ′ Reduced set of invariants1 V’ = V;2 for k = 1 to sizeof(V) - 1 do3 for all vi ∈ V ′ do4 for vj ∈ V ′ do5 if vi is 2(X ⇒ 3Y ) and vj is (2(Y ⇒ 3Z)) then6 Add vnew = 2(X ⇒ 3Z) to V’;7 covers[vnew][vi] ← true;8 covers[vnew][vj ] ← true;9 end10 end11 end12 end13 for all vi ∈ V ′ do14 for all vj ∈ V ′ do15 if covers[vi][vj] == true then16 mark[vj ] = true;17 end18 end19 end20 for all vi ∈ V ′ do21 if mark[vi] == true then22 remove vi from V’;23 end24 end25 return V’;504.1. Approachsecurity and dependability perspective, v1 is a more important invariantthan v1 and/or v2. Violation of v1 results in losing data, however violationof v2 and/or v3, while an indication of incorrect behavior, does not result indata loss. Failing to retrieve consumption data and submitting them to theserver may be mitigated (for at least a limited time period determined bythe storage size) as data is stored in a persistent storage. On the contrary,failing to store data in the persistent storage at the first place may not becompensated for.As demonstrated by the above example, violation of some invariants hasa higher impact compared to violation of other invariants. This becomesspecially important when, due to memory constraints, we are not able tomonitor all the invariants of the system. Therefore, we design an algorithmto consider the importance of invariants with respect to others, when select-ing the ones to be monitored.In the first step, we let the users define H as a binary relationship be-tween the invariants in V . vi H vj states that invariant vi has a higher rankthan invariant vj . We define the following properties for H.(i) vi H vj ∧ vj H vk ⇒ vi H vk (4.1)(ii) vi H vj ∧ vj H vi ⇒ vi = vj (4.2)(i) indicates that H is transitive and (ii) indicates that H is reflective. Theseproperties entail that H defines a partial ordering on invariants in V . Basedon this relation, our goal is to build an IDS D that has the following prop-erties:• P1: For any invariant v and u where vHu, if the D monitors u thenD monitors v as well.• P2: Among all the IDSes that have the above property within mem-ory constraint M , D provides the maximum coverage with respect tocoverage function U as described in Sec. 4.1.1.To understand the intuition behind our algorithm for building the IDS,we present Fig. 4.5. In this example, the system has 9 invariants, and adirected edge from invariant vi to invariant vj indicates that vi has a higher514.1. Approach!"!#!$!%!&!'!(!)!*Figure 4.5: We allow ranking relationship between invariants of the system.An invariant may not be included in the IDS unless all the invariants ofhigher rank are also included.rank than vj . We topologically sort the invariant, and search all subsets ofinvariants that are valid with respect to property P1 above. For instance,selection of {v2, v5, v8} is invalid since v2 is not selected while having a higherrank than v5, which is selected. However, selection of {v1, v4, v7} is valid.Among all the valid subsets, we pick the one that does not exceed availablememory and provides the maximum coverage.The algorithm to build the IDS is presented in algorithm 3. The al-gorithm consists of two functions. In function findStateMachine, we builda bipartite graph g. One part of the graph are the nodes representing thesecurity properties, and the other part of the graph are the nodes repre-senting the invariants that verify those properties. g[i][j] = 1 if and only ifV [i] ∈ τp[j]. This is done in lines 2 through 6. We also build the directedacyclic graph (DAG) R based on relationship H. This is done in lines 7through 9. In R, there is a directed edge from node u to node v if and onlyif uHv. After these steps, in line 12, we call the search function to findthe optimal IDS. search finds the optimal IDS recursively. It starts from anempty set of invariants nodeSet and eventually finds the invariants that giveus the best IDS. As the first step in search function, we calculate the IDSthat can be built based on the current set of selected invariants in nodeSet(line 13). If the memory requirement of this IDS is within constraint M ,and the coverage it provides is higher than the best coverage we have seenso far, we update the variables bestCoverage and bestStateMachine with thenew values (lines 14 to 23). In line 25, we calculate W as the set of all thenodes in R that have no input edges. In other words, their input degree524.1. ApproachALGORITHM 3: Finding optimal IDS, given the memory constraint and theranking relationships between the invariants.Function findStateMachine()Data: V Invariants, P Security properties, M IDS size constraint, U Thecoverage functionResult: A the IDS automaton1 Graph g[][];2 for i = 1 to size of V do3 for j = 1 to size of P do4 if V [i] ∈ τp[j] then5 g[i][j] = 1;6 end7 if V [i] H V [j] then8 R[i][j] = 1;9 end10 end11 end12 A=search(∅, R, V, P, g, M, 0);endFunction search(nodeSet, R, V, P, g, M, bestCoverage)Data: NodeSet Selected set of invariants, R Graph representing the rankingrelationship between the invariants, V Invariants, P Securityproperties, g The bitartite graph representing the relationship betweenthe invariants and security properties, M IDS size constraint, U Thecoverage function, bestCoverage the coverage of the best IDS found sofarResult: bestStateMachine Optimal state machine for monitoring invariants13 A,mem = calculateBuchi(NodeSet);14 if mem ≤M then15 Graph h[][];16 for all pairs of j, k V[j] ∈ NodeSet and pk ∈ χV [j] do17 h[j][k]=1;18 end19 if bestCoverage ≤ U(g,h) then20 bestCoverage=U(g,h);21 bestStateMachine=A;22 end23 end24 W is the set of all v ∈ R that d−(v) == 0;25 for all S[i] ⊂W ∧ S[i] 6= ∅ do26 W ′ = all the nodes in R that are reachable from W − S[i];27 util,stateMachine=search(NodeSetcupS[i], R− S[i]−W ′), V, P, M );28 if util > bestCoverage then29 bestCoverage = util;30 bestStateMachine = stateMachine;31 end32 end33 return bestStateMachine;end534.2. Evaluation(as indicated d− in the algorithm) is 0. Since R is a DAG, it is guaranteedthat we have at least one such node in the graph. The set W is the set ofall the invariants that either nave no other invariants with higher impor-tance, or any invariant that has higher importance than them is alreadyadded to the nodeSet. Since we want to make sure that we do not violatethe importance order (as determined by relation H) when selecting invari-ants, any non-empty subset S[i] of W is a candidate to be added to theset of selected invariants nodeSet. For any selection of S[i] we add them tothe current nodeSet and remove the unselected nodes (W − S[i]), and allthe nodes reachable from them, from R. The reason that we remove nodesreachable from W − S[i] from R is that when an invariant is not selected,any invariant less important than that should not be selected either. Oncewe update nodeSet and R, we recursively call search again. This assuresthat we search through all possible IDSes that satisfy properties P1 and P2stated above. We do these steps in lines 25 through 27. We select the bestIDS according to the coverage function U (lines 28 through 30) and finallyreturn the selected state machine in line 33.Since our algorithm is considering all possible solutions, its time com-plexity is exponential with respect to the number of invariants. The spacecomplexity of the algorithm is O(|V |2).4.2 EvaluationIn this section, we discuss the results of running MaxMinCoverage IDS andMaxProperty IDS on a smart meter platform. We break down RQ2 and layout the following research questions:• RQ2.1 (Detection): What portion of the attacks against SEGMetercan be detected by MaxMin IDS and MaxProperty IDS?• RQ2.2 (Relationship between estimated coverage and attackdetection): How close is the attack detection rate of MaxMinCover-age IDS and MaxProperty IDS at runtime, to their estimated coverageat design time?544.2. Evaluation• RQ2.3 (Effect of increasing memory constraints on the IDS):How does increasing memory constraints affect the detection rate ofMaxMinCoverage IDS and MaxProperty IDS in terms of their com-pliance with their estimated coverage at design time?• RQ2.4 (Performance overhead): What is the performance over-head of MaxMinCoverage IDS and MaxProperty IDS on the system?• RQ2.5 (Effect of invariant reduction on the IDS): How doesperforming invariant reduction before building MaxMinCoverage IDSand MaxProperty IDS affect their coverage at runtime?• RQ2.6 (Effect of invariant ranking on the IDS): How doesadding ranking relationship between the invariants affect the coverageof MaxMinCoverage IDS and MaxProperty IDS for different securityproperties at runtime?4.2.1 Experimental setupWe use SEGMeter, an open source smart meter as a test bed to evaluate ourtechnique for building IDS for embedded devices [77]. Please see Chapter3.2.1 for technical description of SEGMeter. Our IDSes run on the Arduinoboard of SEGMeter. As we are using system calls as propositional variablesin our model, we use strace to create the run-time trace of the software. Atthe boot-up, strace attaches to the process we are monitoring, intercepts thesystem calls and logs them, along with the time and argument information.The second component of our IDS runs in periods of 10 seconds, processesthe log file and compares it to the model of the system. Later in Sec. 4.2.3we explain why the 10-second time interval is chosen.4.2.2 ExperimentsAn attacker may tamper with the meter by exploiting the potential vulnera-bilities in the system. A successful attack results in changing the operationalflow of the software by either executing unintended operations (e.g., deletingdata), or by skipping legitimate operations (e.g., storing data).554.2. EvaluationWe use fault injection to simulate the attacks that result in changing thenormal behavior of the smart meter. The reason for using fault injection isthat we do not have access to any database of known attacks against thesmart meter software. Also, smart meters are relatively new platforms, andwe are interested in evaluating them against unknown attacks as well. Otherhave adopted similar strategies to study effects of attacks. For example,Tseng et. al. [81] have used fault injection to mimic the impact of maliciousattacks against power grid embedded devices such as Real Time AutomationControl (RTAC).We perform the fault injection at the code level using code mutation.Each mutation involves flipping a single branch condition. This way, wesimulate the effect of many attacks by changing the operational flow of thesoftware. This process may not result in skipping/executing the exact opera-tions that the attacker intends to. However, we are interested in evaluatingour IDSes in detecting any changes in the execution flow of the softwareboth due to known and unknown attacks. As we are using fault injectionfor simulating attacks, we use the term attacks, in place of faults, in the restof this section.Property DescriptionHeartbeat Availability Generation of heartbeat messages at specific time intervals.Heartbeat Integrity Correctness of generation of heartbeat messages in terms of length, content, etc.Storage/Retrieval Availability Availability of data storage and retrieval modules of SEGMeter, when requested.Storage/Retrieval Integrity Correctness of storage and retrieval operations to guarantee integrity of data.Time sync. Availability Ability of SEGMeter to synchronize itself with the server timer, whenever required.Time sync. Integrity Correctness of synchronization results.Network Availability Availability of network modules (e.g., when sending/receiving data) upon request.Network Integrity Correctness of networking operations, to guarantee the communication integrity.Command Processing Availability Ability of SEGMeter to process server commands, upon receiving them.Command Processing Integrity Correctness of operations when processing and executing commands.Table 4.2: Availability and integrity properties of SegMeter.We created 226 mutations of the code (for 226 branches). These muta-tions result in breaking the security properties of the meter (unless they arebenign). Based on our observations, the effect of the attacks can be cate-gorized into 7 groups, as shown in Table 4.3. The statistics of occurrencesof each of the categories are presented in Fig. 4.6. Crashing is the mostcommon effect of our attacks. The reason is that in many cases, changing564.2. Evaluation22%31%14%9%12%9%3%  Data lossCrashWrong formatDuplicate dataTiming errorBenignMiscellaneousFigure 4.6: We have cat-egorized the fault injec-tion results into 7 cat-egories. The statisticsof occurrences of each ofthese categories are pre-sented in this figure.020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesDetection(%)Figure 4.7: The detec-tion results of MaxMin-Coverage IDS built using4MB of memory, for at-tacks against different se-curity properties of SEG-Meter.the execution path of the SEGMeter software results in operating on NULLdata, which results in a crash. Also, we list the availability and integrityproperties of SEGMeter in Table 4.2. These properties are affected as aresult of attacks.Fault injection results DescriptionData loss Losing data before it is completely processed, e.g., clearing flash memory data before sending it to the server.Crash Terminating software execution due to exceptions, e.g., operating on nil data in the Lua language.Wrong formatting Changing execution path of the software resulting in incorrectly formatted consumption data.Duplicate data Skipping certain checks (e.g., whether data is stored) resulting in redundant operations.Timing error Failing to execute certain operations (e.g., connectivity check) within a predetermined time frame.Benign Causing no harm when changing the execution flow of the system, e.g., failing to print debug messages.Miscellaneous Other faults, e.g., random cases of failing to send heartbeat messages.Table 4.3: Effects of fault injection on the smart meter software.4.2.3 ResultsSEGMeter is equipped with 16MB of RAM, and about 12MB is used by theOS and the meter software. This leaves 4MB for the IDS. We derived 34invariants verifying 10 security properties of the smart meter (these securityproperties are shown in Table 4.2). Building an IDS for monitoring all574.2. Evaluation020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesCoverageprecision(%)Figure 4.8: The accu-racy of MaxMinCov-erage IDS built using4MB of memory fordifferent security prop-erties of SEGMeter.020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesDetection(%)Figure 4.9: The de-tection results of Max-Property IDS built us-ing 4MB of memory,for attacks against dif-ferent security proper-ties of SEGMeter.020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesCoverageprecision(%)Figure 4.10: The accu-racy of MaxMinCov-erage IDS built using4MB of memory fordifferent security prop-erties of SEGMeter.the invariants results in memory requirement of over 7MB which is notfeasible for our smart meter platform. Therefore, in the first step, we buildMaxMinCoverage IDS and MaxProperty IDS using 4MB of memory andevaluate them. We had to limit the number of the generated states ofthe IDS to less than 55000 states to meet the 4MB memory requirement.We note that given the number of states, memory requirements may varydepending on the programming language used. However, the memory usedis directly correlated with the size of the state machine. Using our testmachine (3.4GHz Intel CPU and 8GB of RAM), we were able to build theIDSes in less than 6 hours in total. We note that this process is offlineand done once for each embedded device. Hence, it is not a significantperformance bottleneck.RQ2.1(Detection): We evaluate the attack detection results of MaxMin-Coverage IDS and MaxProperty IDS. We run our IDSes against the attacksexplained in Sec. 4.2.2. We evaluate the detection as below:detection(%) =number of detected attackstotal number of injected attacks× 100To better understand the results of our IDSes, we present their detec-584.2. Evaluationtion separately for each individual security property. Detection results ofMaxMinCoverage IDS is presented in Fig. 4.7. As explained in Sec. 4.1.4,the goal of MaxMinCoverage IDS is to maximize the minimum propertycoverage among all the security properties. Therefore, in practice we ex-pect that the smallest detection for a security property to be close to theaverage detection among all the security properties. Our results verify thisexpectation. Fig. 4.7 shows that the smallest detection rate for a securityproperty is 70%, while the average detection among all security properties is79.5% (i.e., there is only 9.5% difference between the average and minimumdetection).The detection results for MaxProperty IDS are presented in Fig. 4.9. ForMaxProperty IDS (see Sec. 4.1.4), the number of the security properties thatare completely covered (with property coverage of 100%) are maximized.We estimated MaxProperty IDS to provide property coverage of 100% for 5security properties of the system. Our detection results in Fig. 4.9 verify this.The detection rate of MaxProperty IDS for the other security propertiesranges from 0% to 35%.RQ2.2 (Relationship between estimated coverage and attackdetection): We evaluate the compliance of detection results of MaxMin-Coverage IDS and MaxProperty IDS at runtime, with their estimated cov-erage at the design time. We define accuracy of our IDS for each securityproperty of smart meter using the formula below:accuracy(%) = max(detectionproperty coverage, 1)× 100Accuracy indicates the ratio of detection rate of the IDS to the estimatedcoverage of the IDS. Higher accuracy indicates better compliance of the de-tection results of the IDS with its estimated coverage. In the above formula,property coverage indicates the estimated coverage provided by MaxMin-Coverage IDS or MaxProperty IDS, for each of the security properties inthe system (Sec. 4.1.4 and Sec. 4.1.4). The detection results of the IDS maybe higher than its estimated coverage at design time (due to better perfor-mance than what we estimated) and hence, we have the term max(detection/ property coverage, 1) to have the 100% accuracy as maximum. In the next594.2. Evaluationparagraph we explain why the coverage at runtime may be even higher thanthe estimated coverage.We study the accuracy of MaxMinCoverage IDS for each security prop-erty in Fig. 4.8. We observe that the smallest accuracy is 89%, and theaverage accuracy among all security properties is 97%. This indicates thatdetection of MaxMinCoverage IDS at runtime strongly complies with its es-timated coverage at the design time. In practice, we observed that in manycases the detection rate is even higher than the estimated coverage (leadingto the accuracy of 100%). The reason is that attacks may propagate in thesystem. Therefore, even if an attack breaking a security property is notinitially detected, it may affect other security properties and be detectedlater. In other words, monitoring a security property helps with detectingattacks on other security properties as well.We have presented the accuracy of MaxProperty IDS for all the securityproperties of the system in Fig. 4.10. Our results show that only one securityproperty (command processing availability) has accuracy of less than 100%(which is 77%). This indicates that the detection results for MaxPropertyIDS complies with its estimated coverage at design time. The 77% accuracyfor one property (availability of command processing) is because the invari-ants verifying this property are larger (due to the complexity of the code)and lead to higher number of states compared to other invariants. There-fore, memory constraints result in lower coverage for this property. Thisleads to lower accuracy.RQ2.3(Increasing memory constraints): To evaluate MaxMinCov-erage IDS and MaxProperty IDS under memory constraints, we build theseIDSes using 2MB of memory (severe memory constraint), and 1MB of mem-ory (extreme memory constraint). To address these constraints we limit thenumber of states in our IDSes to less than 22000 states and 13000 statesrespectively. The detection results and accuracy for MaxMinCoverage IDSusing 2MB of memory are shown in Fig. 4.12 and Fig. 4.13. These resultsshow that severe memory constraints reduce the detection rate of MaxMin-Coverage IDS to an average of 44.3%, which is expected due to the smallavailable memory. However, even under severe memory constraints, the es-604.2. Evaluationtimated coverage of MaxMinCoverage IDS is close to its runtime detection,resulting in an average accuracy of 92%. The detection results and accuracyof MaxProperty IDS using 2MB of memory are shown in Figures 4.14 and4.15. These results show that, under severe memory constraints, MaxProp-erty IDS successfully provides 100% detection for three security properties ofthe system, and provides high average accuracy of 93%. This indicates thateven under severe memory constraints, the detection results of MaxPropertyIDS complies with its estimated coverage.We further reduced the available memory to 1MB, which is an extremememory constraint. In this case, as the number of invariants covered in ourIDSes is very small, the detection rate and the accuracy are significantlyreduced. MaxMinCoverage IDS provides an average detection rate of 19.8%,and MaxProperty IDS can provide 100% detection for only one securityproperty. This is not surprising as 1MB is less than 15% of memory requiredto build an IDS monitoring the complete set of invariants of the system.RQ2.4(Performance overhead): Our IDSes read and processes thesystem call log created by strace every T seconds. Smaller T results infaster detection of attacks (as the IDS is run more often), and smaller logfiles. We study the performance overhead of our IDSes, for different valuesof T , in Fig. 4.11. For T = 10 seconds, both MaxMinCoverage IDS andMaxProperty IDS (built using 4MB and 2MB of memory), incur less than7% performance overhead on the system (we do not consider the overhead ofIDSes that operate under extreme memory constraint of 1MB, as it results inlow coverage). We observed that making the intervals too small (<1 second)results in high read/write operations, and higher performance overhead.Also, increasing the time interval beyond 10 seconds does not result in asignificant performance gain. Based on this, we picked 10 seconds as thetime interval for our IDSes. This keeps the size of the log file small (as thesize of the flash memory is limited), results in fast detection of the attacks,and incurs low performance overhead on the system.RQ2.5(Invariant reduction): We ran an invariant reduction pass asstated in Sec. 4.1.5. This resulted in reducing the number of invariants byover 24%. We repeated the process of building MaxMinCoverage IDS and614.2. Evaluation0 10 20 30 40 50510152025Time interval (s)Overhead(%)  MaxProperty IDS (4MB)MaxMinCoverage IDS (4MB)MaxMinCoverage IDS (2MB)MaxProperty IDS (2MB)Figure 4.11: Performanceoverhead of MaxMinCov-erage IDS and MaxProp-erty IDS using differenttime intervals. Making thetime interval too small willincrease the performanceoverhead.020406080HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesDetection(%)Figure 4.12: The detectionresults of MaxMinCover-age IDS built using 2MBof memory, for attacksagainst security propertiesof SEGMeter.MaxProperty IDS based on the reduced set of invariants, and for 4MB and2MB memory constraints. The coverage results for MaxMinCoverage IDSunder 4MB memory constraint is presented in Fig. 4.16. The minimumdetection rate among all security properties is 72%, and the maximum de-tection rate is 100%. The average detection rate is over 84% which shows5 percentage point increase compared to not running invariant reduction.However, under extreme memory constraint of 2MB, invariant reductionresults in significant improvements in detection. The results of buildingMaxMinCoverage IDS after invariant reduction, and using 2MB of memoryis shown in Fig. 4.17. The average detection rate is just over 60% which isa significant improvement compared to average detection rate of 44% whenwe do not run invariant reduction. This shows that under extreme memoryconstraints, we can benefit the most from invariant reduction as the numberof invariants we can monitor is very limited. Invariant reduction results incompacting several invariants into one, and therefore, saving memory while624.2. Evaluation020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesCoverageprecision(%)Figure 4.13: The ac-curacy of MaxMinCov-erage IDS built using2MB of memory, forsecurity properties ofSEGMeter.020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesDetection(%)Figure 4.14: The de-tection results of Max-Property IDS built us-ing 2MB of memory,for different securityproperties of SEGMe-ter.020406080100HeartBeat Av.HeartBeat Int.Storage/Retr. Av.Storage/Retr. Int.Time sync. Av.Time Sync. Int.Network Av.Network Int.Command Av.Command Int.Security PropertiesCoverageprecision(%)Figure 4.15: The ac-curacy of MaxPropertyIDS using 2MB ofmemory, for differentsecurity properties ofSEGMeter.providing higher coverage. This becomes more important as we have lessmemory available.Invariant reduction improves detection results for MaxProperty IDS aswell. We have presented the detection results for MaxProperty IDS using4MB of memory, after invariant reduction, in Fig. 4.18. We can see thatinvariant reduction allows us to completely cover the invariants that verifyintegrity of storage/retrieval component. Compared to no running invariantreduction phase, we can still completely verify integrity of storage/retrievalcomponent even when use only 2MB of memory (Fig. 4.19), and also signifi-cantly improve detection rate for availability of storage/retrieval component.Moreover, these results show that substituting several invariants with oneby taking advantage of their transitive relationships, does not negativelyimpact coverage.RQ2.6(Effect of invariant ranking on the IDS): Based on the al-gorithm provided in Sec. 25, we created a relationship between invariantsverifying the availability and integrity of networking operations and the in-634.2. Evaluation020406080100Detection (%)Security PropertiesFigure 4.16: The detec-tion results of MaxMin-Coverage IDS after in-variant reduction, andusing 4MB of memory.020406080100Detection (%)Security PropertiesFigure 4.17: The detec-tion results of MaxMin-Coverage IDS after in-variant reduction, andusing 2MB of memory.020406080100Detection (%)Security PropertiesFigure 4.18: The de-tection results of Max-Property IDS after in-variant reduction, andusing 4MB of memory.020406080100Detection (%)Security PropertiesFigure 4.19: The de-tection results of Max-Property IDS after in-variant reduction, andusing 2MB of memory.020406080100Detection (%)Security PropertiesFigure 4.20: Thedetection results ofMaxMinCoverage IDSin the presence ofinvariant ranking, andusing 2MB of memory.020406080100Detection (%)Security PropertiesFigure 4.21: Thedetection results ofMaxProperty IDS inthe presence of invari-ant ranking, and using2MB of memory.variants that verify availability and integrity of time synchronization prop-erties. We considered network-related properties to be more important asthey interface with users and therefore, are considered a clear attack surface.However, while failure of time synchronization affects time-of-use billing, theconsequences are limited (billing is still possible). Given this relationshipbetween the invariants, we build MaxMinCoverage IDS and MaxPropertyIDS, using 4MB and 2MB of memory, using algorithm 3. We did not runan invariant reduction phase to make sure that we are isolating the effect ofinvariant ranking. Using 4MB of memory, MAXMinCoverage IDS detected644.3. Summaryall the attacks targeting availability and integrity of networking operations.This shows 31% increase compared to the previous results in Fig. 4.7. Onthe other hand, the average coverage for time synchronization operationsis reduced by 19%. The coverage results for MaxProperty IDS using 4MBof memory does not show a noticeable change compared to Fig. 4.9 as net-working operations are already 100% covered.The detection results for MaxMinCoverage IDS using 2MB of memoryis presented in Fig. 4.20. We observe that 100% of the attacks targetingnetwork availability and integrity are detected while the detection rate oftime synchronization properties is reduced. We note that the average attackdetection rate for network operations using our initial algorithm with 2MBmemory constraint is less than 60% (Fig. 4.12). This implies that the spacein the IDS model has been assigned to invariants verifying network propertiesat the expense of time synchronization properties, which is our desire. Thedetection results for MaxProperty IDS using 2MB of memory is presentedin Fig. 4.21. Compared to having no relationships between the invariants,we observe that detection for network availability property reaches 100%.We also note that the coverage for time synchronization integrity has beendropped. This is a positive result as this was our intention when definingthe ranking relationships.These results indicate that using algorithm 3 provides the developers ofIDSes with control over deciding what invariants (and as a result, securityproperties) have higher importance. Therefore, The decisions of the IDSdeveloper result in having an IDS that has the desired runtime behavior.4.3 SummaryIn this chapter, we formulated the problem of building IDS for embeddedsystems as an optimization problem. Given the memory constraints of thedevice, the set of security properties and the invariants of the system ver-ifying those properties, we build an IDS within the memory constraints ofthe device that maximizes the coverage for the security properties.Using our technique, the user may define their own coverage function654.3. Summaryand use it to build an IDS. The security of the system is dependent on thevalidity of its security properties and invariants. Our formulation allows anymonotonic coverage function defined over the graph of security properties P ,and the set of invariants V , defined over single and linear executions, thatverify those security properties. Examples of coverage functions other thanthe ones presented in this chapter would be number of selected invariants,and average number of invariants selected per security property.66Chapter 5Security AnalysisIn this chapter, we aim to develop techniques for analyzing security of agiven class of embedded devices and generate attacks against them, in orderto improve their security. This chapter addresses RQ2 laid out in Chapter1.5: How can we automatically analyze security of embedded systems withrespect to the extended accesses the adversaries have to them? Each class ofembedded systems, e.g., smart meters, share significant similarities in design,regardless of the vendor. Therefore, we propose two analysis techniques inthis chapter. The first approach is a design-level analysis technique thatformally analyzes the common specifications of a class of embedded systems.This approach allows the developers to find shortcomings of the design inproviding security, and address them in the implementation phase. This isimportant as accounting for bugs after implementation is significantly moreexpensive. It may require changes in the design, major changes in the codeand updating already-deployed devices. The second approach is a code-levelanalysis technique. Finding shortcomings in the design does not guaranteethat the implementation will be bug-free. Hence, we propose a code-levelanalysis technique as well, to find attacks against the implementation of thesystem.Initially, we were skeptical of performing direct analysis on the codedue to the problem of state-space explosion. To our surprise, our code-levelanalysis technique proved to be more efficient than design-level analysis. Wewill discuss this is more details later in the chapter.In this chapter, for the purpose of accurate evaluation, based on thethreat model presented in Chapter 1.4, we define a set of concrete ac-cesses and abilities for the attacker. We assume that the attacker may haveread/write access to the communication interfaces of the embedded system.675.1. BackgroundAccess Actions- Tampering with thecover sealA1 Physical access - Observing visibleto the device indicators- Disabling internalbatteryA2 Physical access to theinternal/external - Send/Receive data viacommunication interfaces communication interfacesA3 Access to a routingnode in the grid network - Dropping data packetsinfrastructureTable 5.1: Accesses and capabilities of the adversaryTherefore, the attacker may intercept data sent from the system, and send(incorrect) data to the system. We also assume that the attacker may havephysical access to the system and perform actions such as rebooting the sys-tem (e.g., powering it on/off). Furthermore, we assume that the attackersmay intercept communication of the meter, for example, by obtaining accessto some node on the grid network. This is a realistic assumption as it hasbeen shown that the complexity and the scale of smart grid infrastructureprovides several entry points for attackers to obtain such access [62]. Basedon this, we assume an attacker may 1) drop messages communicated to thedevice’s interfaces, 2) replay messages to the device’s interfaces, and 3) re-boot the device at any point in time. We have presented the summary ofaccesses and capabilities of the adversary in Table 5.1.In this chapter, first we explain our design-level analysis technique. Thenwe present our code-level analysis techniques and finally, we evaluate bothtechniques on SEGMeter.5.1 Background5.1.1 Characteristics of embedded devicesUnlike data centers, web servers, and other isolated computing machines,embedded devices are physically integrated with everyday lives of their users.685.2. Design-level analysisExamples of the embedded devices that have proximity to the users aresmart meters, smart car controllers, and implantable medical devices. Thisresults in higher accessibility for these devices. Therefore, attackers target-ing embedded devices have more options available to them to interact withthe device and to tamper with them, compared to a remote server. Forexample, attackers may physically reboot a device, or feed them data viatheir communications interfaces. In this chapter, we pick one class of theseembedded devices as a testbed, namely smart meters.5.1.2 Security invariantsAn attack against a system is a series of operations by an attacker that leadto violation of security invariants of the system. These invariants may verifyintegrity, and/or availability of the system. Our approach is not bound tospecific security invariants and the users of our technique may define theirown invariant sets based on the properties of the system. They may also useinvariant mining tools such as Daikon [30]. For using our code-level analysistechnique, the users must write assertions that verify the security invariants,and insert the assertions in code. This is reasonable as different securityinvariants translate to different assertion checks. Therefore, it allows theusers of our technique to consider security invariants of their choice, and thecorresponding assertions. Failure of the assertions indicates an attack thatviolates security invariants of the system.5.2 Design-level analysisIn this section, we propose a formal approach for analyzing security of smartmeters at design level. We define a formal model for smart meters, a setof basic actions for an attacker, and use model checking to automaticallysearch all the possible scenarios of applying those actions on the model ofsmart meters. The search finds the scenarios that lead to potential software-interference attacks, and is guaranteed to find all the software-interferenceattacks within the state space of our model (both the smart meter and the695.2. Design-level analysisattacker).We follow a three step process for building the model as follows. In therest of this section, we explain each of the steps in more detail.• Step 1: We formally model the components of smart meters and theiroperations. Smart meters are computing devices and can be consideredas small general purpose computers. However, unlike general purposecomputers, smart meters have low memory, low computing-capacity,and are designed to carry out a specific set of operations. In Chapter3, we use an abstract model for operations of smart meters. This ab-stract model represents an implementation-independent model of thecomponents of the meter, their operations, and their execution order.In this section, we express the abstract model formally in rewritinglogic. Rewriting logic lets us model all the operations (functions) ofthe system, and the transitions between its states.• Step 2: We define a set of capabilities for the attacker also in rewritinglogic. Modeling both the smart meter and the attacker’s capabilities inrewriting logic allows us to automatically and systematically search forall the possible scenarios in which the attacker’s actions on the metercan take the system to an unsafe state. An example of an unsafe stateis when consumption data calculated by the meter are lost, and notsubmitted to the server. The users of our model may define their ownunsafe states as a first order logic formula over the states of the model.• Step 3: We compose the model of the smart meter, concurrently withthe model of attacker actions. Using model checking, our systemsearches through all the execution paths of the models that lead tounsafe states. The actions that take the smart meter into an unsafestate will be identified as a potential software-interference attack onthe system. Because we use model-checking, we are guaranteed to findall the possible paths that may take the system into an unsafe state,within the scope of the model.705.2. Design-level analysis5.2.1 Rewriting logicIn this section, we use Rewriting logic [59] to formally model smart me-ters and attacker capabilities. Rewriting logic is a flexible framework forexpressing proof systems. It allows us to define the transitional rules thattransition the system from one state to another, as well as the functionsdefined in the system. Using rewriting logic, we can specify the behavior ofthe system as a series of states, functions, and rules of transitioning betweenthe states. Also, we can query the transition paths of the system to verifythe correctness of the system behavior.Formally a rewrite theory is a 4-tuple < = {Σ, E, L,R}. Σ is the setof all functions (operations), and constants defined in <. E is the set ofall the equations in <. Equations help define the operation of the system(for example how two variables are added together). R is a set of labeledrewriting rules and L indicates those labels. Rewriting rules model transi-tions in the system and express the way the system evolves. In a rewritetheory, any of the rewrite rules may be applied concurrently to representthe behavior of a system. This lets us build rules that capture the behaviorof both the system and the attacker. Using model checking, we can check ifany sequence of the attacker’s rewrite rules together with the rewrite rulesof the smart meter can transition the system to an unsafe state.In this section, we implement the formal model of the system in rewritinglogic using Maude [24]. Maude is a tool that supports rewriting logic, andenables the users to both execute rewriting logic rules and formally verifythem. This is useful as we can execute the model to gain confidence in itbefore formally verifying it.Maude allows us to perform model checking of the system with regardto invariants. This means that we can check whether it is possible that froman initial state s in the model, we can reach a state x, in which an invariantI does not hold true. In Maude, this is done by using search command:search(s) ⇒ x such that I(x) 6= true. The invariant I (e.g., data beinggreater than or equal to 0), may be defined by the user of the system, andwe define state x in which the invariant I does not hold as an unsafe state.715.2. Design-level analysisMaude executes the search by doing breadth-first-search, starting frominitial state s, and applying one rewriting rule at a time to the previous state.This way, all possible transitions in the model are checked. This is knownas explicit state model checking (ESMC) [10]. Note that other variants ofsearch strategies are possible in Maude e.g., symbolic model checking [10],that aim to tackle the problem of state space explosion that ESMC incurs.We do not explore these in this section as the state space of the smart meterwas still amenable to be analyzed by ESMC within a reasonable amount oftime, as shown in Sec. Formal modelWe use the abstract model of smart meters used in Chapter 3 as our inputto build the formal model of smart meters in rewriting logic. This abstractmodel presents an implementation-independent model of the components ofthe meter, their operations, and their execution order. Therefore, it is validfor different implementations of smart meters. Using the abstract model,we extract the execution paths of components of the meter, and formallydescribe them. Below, we briefly explain the major operations of a smartmeter as per the abstract model.Smart meter’s operations: Upon starting, the meter initializes thesensors and communication interfaces. The microcontroller periodically col-lects data from all the sensor channels by polling them, and averages datasamples to calculate consumption data for each channel. Then, the micro-controller listens to incoming data requests from the communication unit,via a serial interface. Upon receiving a data request, consumption data cal-culated so far are sent to the communication unit of the meter, which storesthe data on physical storage. The meter verifies connection to the networkand to the server by pinging the server periodically. At specific time inter-vals, the meter retrieves all the unsent consumption data from the physicalstorage and transmits them to the utility server via its network interface.The communications unit of the meter also periodically checks for any inputcommands that may be sent from the utility server. The meter parses and725.2. Design-level analysisMicrocontrollerStore data on physical memoryRetrieve data andsend them to the serverUtility serverSensorsData overserial interface Network1 2 3Smart MeterFigure 5.1: In this section, we discuss and formalize the first two executionpaths of the smart meter, shown in this figure.verifies any incoming command from the server, and executes them.We explain the formal model for two parts of the smart meter mentionedabove. These parts include: 1) passing the consumption data from themicrocontroller to the communication unit the meter, and 2) storing dataon the flash memory before submitting it to the utility server. These pathsare shown in Fig.5.1. For clarity and simplicity, we omit some details of themodels.Passing consumption data to the storage componentA smart meter has a number of sensor channels. A microcontroller peri-odically reads each of these channels in a loop, calculates the consumptiondata associated with them, and produces a stream of sensor data. Belowwe discuss the formal model for production of a stream of sensor data re-sulting from sensor channels in the meter. The illustration of sensor data ispresented in Fig. 5.2. Sensors produce data tuples that indicate the indexof the sensor and its value. A list of data is formed by putting these tuplestogether.The formal model of sensor data is shown in Fig. 5.3. In line 2 ofFig. 5.3, we define SensorElement, SensorList, SensorNumber, and Sensor-Value. These are the data types that we use to formally define sensor data735.2. Design-level analysisMi cr oc on tr ol l erS en so rs… ൏ ݏ௜భ, ݒ௜భ ൐	൏ ݏ௜మ, ݒ௜మ ൐	൏ ݏ௜య, ݒ௜య ൐ 	…SensorElementSensorListFigure 5.2: SensorList is a series of SensorElements and is the result ofmicrocontroller operations.SENSOR-DATA1. fmod SENSOR-DATA is 2. sort SensorElement SensorList SensorNumber        SensorValue.   3. op sensorElement : Nat Nat —> SensorElement.4. op __  : SensorList SensorList —> SensorList.5. op hasSensor : SensorList Nat—> Bool.6. var r n t : Nat.7. var dataList : SensorList.8. eq hasSensor(sensorElement(r, n) dataList, t) =       if r==t then true else hasSensor(dataList,t) fi.9. endfmFigure 5.3: Formal model of sensor data in Maude.and the operations on it. In Maude1, each of these types is called a sort.Each sensor element is a tuple < s, v > (as shown in Fig. 5.2), which is theresult of the operations of the microcontroller on sensor channels. s indi-cates the channel index, which is of type SensorNumber, and v indicates itsvalue, which is of type SensorValue. This tuple is formally defined in line 3,by putting two natural numbers (indicated as ’Nat’) together. A stream ofthese tuples forms SensorList, which is defined in line 4. SensorList is simplybuilt by putting a series of SensorElements together. In line 8 of Fig. 5.3, wedefine a common operation on the sensor data: hasSensor. This operationverifies whether a stream of sensorElements (i.e., sensorList), contains dataassociated with a specific sensor index, and is defined recursively.After defining the sensor data in a smart meter, we present the rules1We present a brief primer on Maude in Appendix B.745.2. Design-level analysisSENSOR-STATES1.mod SENSOR-STATES is2.op getSensorDataList : —> SensorDataList.3.var dataList : SensorDataList.4.var r n : Nat.5.rl [r1]:getSensorDataList —> sensorDataElement(0,0).6.crl[r2]:sensorDataElement(r,n) —>    sensorDataElement(r,n) sensorDataElement(r+1, 0)    if r < maxSensorNumber.7.crl[r3]:sensorDataElement(r,n) —>   sensorDataElement(r,n+1) if n < maxSensorData.8.endmFigure 5.4: Formal model of states of sensor data in Maude.that define their production in Fig. 5.4. We define the production of sensordata using a recursive rule. At each step of the recursion, we either createa tuple of sensor data for a new sensor channel (line 6), or create a newvalue for an existing sensor channel (line 7). Line 5 is simply the base caseof recursion representing a tuple of sensor data for channel 0. The modellets us define a limit for the number of sensor channels, which is not shownhere. The number of sensor channels depends on the specific model of themeter.Receiving and storing sensor dataAfter a stream of sensor data is produced by the microcontroller, it is re-ceived by another process which is in charge of storing them. This commu-nication is via a serial interface. The receiver process sends a data requestmessage to the microcontroller, and waits for a response. If there is anysensor data available, the microcontroller sends the data, otherwise no datais sent and the request times out.The state diagram of this procedure is based on the abstract model and isshown in Fig. 5.6. The formal model for receiving sensor data correspondingto the state diagram is shown in Fig. 5.5. First, the receiver process creates asocket to communicate with the microcontroller (line 6). This corresponds tostates 1 and 2 of Fig. 5.6. Next, a request is sent (via askForData operation)755.2. Design-level analysisRECEIVE-SENSOR-DATA1. mod RECEIVE-SENSOR-DATA is2. sort DataReques.3. var s: Socket.4. var request: DataRequest.5. var dataList: SensorDataList.6. rl [l1]: startReceivingSensorData —> createSocket.7. rl [l2]: s —> askForData.8. rl [l3]: request —> waitForSensorData.9. rl [l4]: waitForSensorData —> dataList.10.rl [l5]: waitForSensorData —> timeoutSensorData.11.endmFigure 5.5: Formal model of receiving sensor data from the notify the microcontroller that it is expecting to receive sensor data (line7). This step corresponds to state 4 of Fig. 5.6. Then the receiver processwaits for data (line 8). This corresponds to state 5 of Fig. 5.6. Eventually,either a stream of sensor data is received (line 9), or the request times out(line 10). These steps correspond to states 6, and 7 of Fig. 5.6.After sensor data is received, it will be stored in the flash memory. Wemodel this process by changing the state of each tuple of sensor data (knownas sensorDataElement), to a new tuple, namely storedDataElement. Simi-larly, a stream of storedDataElements will form storedDataList. We presentthe formal model for representing data storage in Fig. 5.7. In this figure, wedefine the types StoredDataElement which is a tuple similar to sensorDataand StoredDataList, which is a stream of StoredDataElements (lines 2-5). Inline 8 of Fig. 5.7, the transition of the state of data is defined. The way thistransition works is that in the sequence of received sensor data, we changethe state of each tuple of sensor data to a tuple of stored data. Eventually,the meter will have a sequence of stored data that it has received and notyet sent to the server (in the absence of attacks).5.2.3 Attacker modelWe formally define actions for dropping messages, rebooting and restartingthe system (to interrupt data flow and message processing), and replaying765.2. Design-level analysis1-Start receiving sensor data2-Create a socket3-Quit4-Request for data5-Wait for data6-Timeout7- Receive sequence of dataFailedSuccessfulFigure 5.6: SensorList is a series of SensorElements and is the result ofmicrocontroller operations.STORE-SENSOR-DATA1.mod STORE-SENSOR-DATA is2.sort StoredDataElement.3.sort StoredDataList.4.op storedDataElement : Nat Nat —> StoredDataElement.5.op __ : StoredDataElement StoredDataList —>          StoredDataList.6.var r n : Nat.7.var l : StoredDataList.8.rl [r1] : sensorDataElement(r,n) l —>            storedDataElement(r,n) l.9.endmFigure 5.7: Formal model of storing sensor data received from the micro-controller.775.2. Design-level analysisa message. These actions are simple and can be done by ordinary users ofsmart meters. It is possible to extend the set of attacker actions to moresophisticated ones.We present the formal rules for the attackers’ action in Fig. 5.8. Droppinga message is defined in line 8 of Fig. 5.8 for dropping SensorDataElements.The complete set of rules include other communication protocols of themeter. As a result of this rule, any element of sensor data, at random, maybe dropped by an attacker.Line 9 presents the general rule for rebooting the system. This actionmay correspond to simply rebooting the meter by unplugging it from powerand plugging it back in. To define this action, we define an extra operationreboot. At any state s, we can transition to a reboot state from the currentstate s. For instance, while the system is generating a series of sensor datatuples, transitioning to the reboot state will interrupt the normal executionpath as the rules for generating sensor data cannot be applied anymore.This action can hence lead to data loss.Line 10 presents a rule that lets the system go from current state c to aprevious state p. This transition is not part of the legitimate flow of the sys-tem. p is replaced by any state in the system that involves communication.By transitioning back to such a state, the model can re-execute the com-munication procedure. This rule models an attacker that replays messagessent between components of the meter via its interfaces, e.g, serial interface.Equation before in line 10, will return true, if state p is a prior state.By adding these extra actions to the rules of the system, we are able tosearch through the execution steps and verify whether we can reach unsafestates. Examples of unsafe states are those in which produced sensor dataare not stored on flash, and transitioning to a data submission state whilethe socket is closed. Note that not all the unsafe states produced necessarilyrepresent a feasible software-interference attack on the real smart meter. Wediscuss this in more detail in Sec. 5.4.Mapping the results of formal analysis to the code: We need tomap the results of the formal model back to the meter’s code to mount theattacks. To facilitate the process of mapping the results of the formal model785.3. Code-level analysisATTACKER-ACTIONS1. mod ATTACKER-ACTIONS is2. op crash : —> state.3. var num : NodeNumber.4. var val : Nat.5. var element : SensorDataElement.6. var list : SensorDataList.7. var s c p : State.8. rl [DropMessage] : element list —> list.9. rl [Reboot] : s —> reboot.10.rl [Replay] : c —> p if before(c, p).11.endmFigure 5.8: Formal model of the attacker the code, we developed a semi-automated tool. The input to the tool isL = (r1, r2, ..., rn), a sequence of rewrite rules ri, 1 ≤ i ≤ n that lead to anunsafe state. The output of the tool is the execution paths of the code thatmay represent L. The process is semi-automated at present, as the user ofthe tool needs to manually match the first and the last rewrite rules (r1 andrn) to two nodes of the control flow graph, v1 and v2. This can be done byproviding the id of the rewrite rule and the corresponding function name inthe code that implements the rule. The tool performs simple graph traversaland generates the paths between v1 and v2 in the control flow graph. Theserepresent the viable paths corresponding to the input L, and are returnedto the user. We used this semi-automated tool to translate the results offormal analysis to the meter’s code.5.3 Code-level analysisIn this section we explain our technique for finding software-interferenceattacks against the system at the code level. We model attacker actions ina novel way which allows us, via symbolic execution, to exhaustively search795.3. Code-level analysisfor all the ways an attacker may interfere with execution of the softwareduring rum-time. Our technique finds the interactions that lead to breakingsecurity invariants of the system, and identifies these as software-interferenceattacks.5.3.1 OverviewWe follow a two-step approach to find software-interference attacks againstthe system:• Step 1 - Code Transformations: A software-interference attack isa result of one or more actions taken by an attacker, e.g., droppingmessages, replaying messages. The operations for the first step ofour approach are shown in boxes 1 and 2 of Fig. 5.9. In this step,we define a set of functions that represent attacker actions and injectthese functions in the source code. We define these functions in such away that they may be dynamically activated/deactivated during run-time. This allows us to consider all different ways an attacker mayinteract with the system. We call the code resulting from injectingattacker actions, the transformed code.• Step 2 - Finding Attacks: This step is shown in boxes 3, 4, and5 of Fig. 5.9. The developer of the system (who wants to analyzeits security) may define a set of assertions that verify security invari-ants of the system (see Sec. 5.1.2). The user of our technique injectsthese assertions in the transformed code. Our technique uses a sym-bolic execution engine to symbolically execute the transformed codeand finds out whether there exist any execution flow in the code thatviolates the security assertions. The output of this step would be aset of inputs to the system that lead to violating security invariants.We translate this set of inputs to software-interference attacks thatan attacker may mount on the original system to successfully interferewith the software’s execution.In the next section we explain these steps in more detail. We use SEGMe-805.3. Code-level analysis1- Define	functions	representing	attacker	actions2- Inject	attacker	actions	into	the	source	code4- Symbolically	execute	the	transformed	code5- Find	execution	scenarios	that	attacker	breaks	security	invariantsSource	codeDeveloper-defined	AssertionsTransformed	codeInputOutput3- Inject	assertions	into	the	transformed	codeInputInputStep	1Step	2Figure 5.9: Overview of our technique to find software-interference attacksagainst the system.ter, which is a smart meter from Smart Energy Groups [77] in our examples.5.3.2 Problem formulationWe denote the program running on the device as P . We also assume thatthe attacker is capable of mounting a set of actions A = {a1, a2, ..., ak} onP . These actions may include dropping messages, and rebooting the system.Each of these actions, interfere with execution of P and change its behavior.V = {v1, v2, ..., vm} denotes the set of security invariants that must holdtrue for P . We show execution of P with respect to input I and attackeractions Ai ⊂ A, satisfies the set of invariants ν ⊂ V as hold(PI,Ai , ν) = true.We call M(P ), to be a transformation of P , if the following conditionshold: 1) The set of security invariants for P is equivalent to the set of securityinvariants for M(P ), and 2) For any set of inputs and attacker actions onP that result in violating a subset of security invariants in P , there exists aset of inputs for M(P ) that result in breaking the same subset of securityinvariants and vice versa. More formally, we can write these conditions as815.3. Code-level analysisfollows:∀ν ⊂ V ∃I, Ai ⊂ A⇒ [hold(PI,Ai , ν) = false⇐⇒ ∃I ′ ⇒ hold(M(P )I′,∅, ν) = false] (5.1)Any modification to program P that satisfies the above two conditionsis a valid transformation of P . In the first step we want to find such a trans-formation. In the second step we analyze M(P ) as a stand-alone program,find execution instances that result in breaking its security invariants. Theseexecution instances, may be translated back to an execution instance of Pand a set of attacker actions that interfere with the software and lead tobreaking the same security invariants in P .5.3.3 Step 1: code transformationTo find software-interference attacks against the system, we mount attackeractions on the source code. This means that we insert code snippets toreset variables to NULL, reboot the system, or re-send messages, to accountfor attacker actions that drop messages, rebooting, and replaying messages.However, due to structures such as branches and loops, there are manyrun-time possibilities to invoke attacker actions within code paths. In thissection we discuss how we inject attacker actions in the code so that wesearch all possible scenarios an attacker may perform at run-time.We define an attacker action A as a triplet A =< l, e, t >. l denotesthe instruction after which, either data or execution flow changes due toattacker action. In other words, l indicates the location in the code theattacker affects. e denotes the change in data or control as a result ofthe attacker action. Examples of this include setting a value to NULL, orjumping to an arbitrary location in code. t indicates the time the attackeraction happens.Fig. 5.10 shows the high-level representation of attacker action injec-tion. We explain the procedure in more detail. To define each attackeraction, we define elements l, e, and t. For any action, l is a set of tuples< si, pi > where si is a instruction in the code, and pi determines whetherthe attacker action must be applied before or after si. We define wildcard ’*’825.3. Code-level analysis…!"#$!if	the	next	boolean value	read	from	‘stream’	is	truef()endif…A=<{<!"#$!, after>},	f(),	‘stream’>ProgramFigure 5.10: High-level representation of attacker action injection in place of si to denote that an attacker action may be applied before/afterany instruction. An example of this scenario is rebooting a device when anattacker has physical access to the system. For simplicity, here we considerthe representation of the code in a high-level language (e.g., C, C++, Lua,etc.) as the granularity for l. We made this choice to simplify implementa-tion and decrease performance overhead, while still keeping high granularityfor l. However, our technique can also consider machine-level instructionsas the granularity for l.For example, if an attacker is capable of dropping messages sent to/fromthe device, the location l in which the software-interference attack manifestsitself is before/after send/receive system calls. Therefore, we will have:l = {< send, before >,< receive, after >} (5.2)e represents the effect of attacker action at run-time. It may be any changein data and/or execution flow. Therefore, we define it as a function thatimplements the effect of attacker action. The arguments of the functionare the return values of the instructions listed in l. The argument set maybe empty if there exist no return values. For example, dropping a messagebefore it is received, may result in the return value of NULL. In this scenario,e will be a function taking one argument, which is the result of receive(), andsets it to NULL. We define t as a boolean stream deciding the time attackeraction A occurs. A control function, at locations indicated by l, simply readsa boolean value from the input stream, deciding whether function associatedwith e must be invoked.835.3. Code-level analysisWe explain attacker action injection further with an example. Figure5.11 presents an example attack. The corresponding codeA = 〈{〈http.reques, after〉},alt request(body, code, header, status), drop stream〉 (5.3)which allows malicious users to drop an http response. In this example, lindicates that the attacker action is injected after ’http.request’ instruction.e indicates the pointer to function ’alt request’() that implements the effectof attacker action. t refers to file ’’ which contains the booleanvalues determining the times the attacker action must be invoked. In Figure5.11, the code segment we inject an attacker action into is presented in box3. As determined by l and t, and e, we inject the functions ’control()’and ’alt request()’ after ’http.request’ instruction. At, run-time, every timethe execution flow reaches this location, a new boolean value is read from’’ and is returned as the value of ’control()’. If the value is true,’alt request()’ is executed, which sets the response of ’http.request’ to nil.This is what happens when in fact no response is received (which is the casewhen the attacker drops the response). If the value read from stream isfalse, no extra action is taken and the execution flow continues as normal.As the example shows, by injecting the function ’alt request()’ at the rightplaces, and using boolean streams, we can represent all the ways in whichan attacker may drop the ’http’ response to our system at run-time.5.3.4 Step 2: finding attacksAs we stated before, our goal is to find software-interference attacks onthe system. This means finding actions an attacker must take, at certaintimes, so that security invariants of the system are violated. In the previoussection we injected code snippets, corresponding to the attacker’s actions,in the code base. We also introduced streams of boolean values into theinput. The assignment of different boolean values to the introduced streamsrepresent different actions taken by the attacker at run-time, and covers theentire space of attacker actions.A sequence of attacker’s actions leads to a successful attack, if it violates845.3. Code-level analysisalt_request(body, code, header, status)   return nil;}control() {file =“”)for i = 1 to nfile:read()endx = file:read()n = n + 1file:close()return x;}. . .body, code, header, status = http.request{. . .}if control() == 1 thenbody = alt_request(body, code, header, status)end. . .if body == nilresponse = nilend. . .return responseControlling	t the	time	of	attack	Injecting	e,	the	effect	of	attackLocation	l of	attack,	afterhttp	request	instructionStream	of	boolean values	to	control	the	time	of	attack001110111…123Figure 5.11: ’alt request()’ represents action of an attacker that is capableof dropping http response or more of the security invariants of the system. For every securityinvariant in the system, the user of our technique needs to introduce asser-tions in the code. These assertions verify the state of files, network ports,or values of sensitive data.Given this setup, any set of input values that lead to violating the as-sertions, correspond to a successful software-interference attack that maybe mounted on the system. We explain this with an example. Fig. 5.12,presents an execution path in the code in which, attacker action for drop-ping http response messages has been injected. In lines 1, 2, and 4, thefunction calls ’heartbeat handler()’, ’do sendable()’ and ’check time()’, sendand receive http requests and responses. The piece of code that handlesthe http communication is shown in Fig. 5.11. ’heartbeat handler()’ sendsheartbeat messages to the server to show that the meter is up and run-ning. ’do sendable()’ sends consumption data to the server. ’check time()’performs time synchronization with a time server.In lines 8 and 9, the user of our technique adds an assertion check toverify that the system is not stuck in the loop. Parameter ’max’ may beadjusted according to the acceptable delay. Assuming ’max=5’, assertion in855.3. Code-level analysis1.				success	=	heartbeat_handler()...2.				sent	=	do_sendabale(data)…3.				while	time_is_ok ==	false	do…4.										time_is_ok =	check_time()				5.										if	(time_is_ok ==	true)	then…6.										else...7.									end8.									assert(counter	<	max)9.									counter=counter+110.		endsending	http	request	messageChecking	invariant	violationFigure 5.12: By symbolically executing the code, we find out how attackeractions may lead to violating security invariants in the code.line 8 of Fig. 5.12 will be violated, if we let the values read from ’’in Fig. 5.11 be false, false, true, true, true, true, true, true. We note thatchanging either of the first two values to true (which leads to failure ofheartbeat and data communication) may change the execution path fromwhat we are considering in Fig. 5.12 (for simplicity, the alternative pathsare not shown).By observing the values read from ’’, we can infer what theattacker has to do to mount an attack that violates a security invariant. Inthis example, the attacker must let the heartbeat and data message/responsepass through intact, and drop the response for time synchronization mes-sages 5 times in a row.To find the input values (including the boolean streams) that lead toviolating the security invariants, our system symbolically executes the codeinjected with attacker actions. Symbolic execution analyzes the code tofind the input values that lead to execution of different parts of the code.There are many existing symbolic execution engines that we can use forthis purpose. We are interested in input values that result in violation ofsecurity invariants (assertions in the code). The values of boolean streams865.4. Evaluationin every set of input that leads to violation of security invariants determinethe actions the attacker must take to mount a software-interference attackon the system.5.4 Evaluation5.4.1 Research questionsIn this section, we evaluate our techniques for finding software-interferenceattacks at design-level and code-level for embedded systems. To addressRQ2 from Chapter 1.5, we lay out the following questions:• RQ2.1 (Performance): Using our techniques, how long does it taketo analyze the code?• RQ2.2 (Comprehensiveness): How many software-interference at-tacks do our techniques find against a real smart meter?5.4.2 TestbedSmart meter: We evaluate our technique for finding software-interferenceattacks on SEGMeter, an open-source smart meter from Smart EnergyGroups [77]. Please see Chapter 3.2.1 for technical description of SEGMeter.Analysis platform: We ran the analysis on a Linux machine equippedwith 16 GB if RAM and 3.4 GHz CPU. To run symbolic execution, weuse SymbolicLua [79], a dynamic symbolic execution engine for Lua (as thesmart meter’s code is written in the Lua language). SymbolicLuca uses Z3[27] as its SMT (Satisfiability Modulo Theory) solver. We stubbed out theexternal dependencies such as server calls to create a stand-alone programfor performing the analysis. For the sensor board’s code that is in the Clanguage, we used Clang’s static analyzer, which has a symbolic executionengine [23].875.4. Evaluation5.4.3 Performance (RQ2.1)In this section, we first present the performance results for our design-levelanalysis technique and later, discuss the performance results of our code-level analysis technique.Design analysisWe measure the time taken to run the searches associated with each attackeraction in Maude, along with the number of attack paths for each actionfound by the model in Table 5.2. As can be seen, the time varies widelyfrom a few seconds to a couple of hours depending on the kind of attackand the attacker actions. As expected, the larger the state space exploredby the search queries, the longer it takes for the search. The search for theeffects of dropping packets takes the least time (7 seconds) as it only affectsthe messages sent/received between the meter components and the server,and as each message has only two states, namely dropped or unchanged.However, the search for the effects of system reboot takes about 2 hours asthe system can be rebooted (or not), at every state in the state space of themodel, which are much more numerous than messages.Table 5.2 shows that when the attacker action affects a larger state space(such as system reboot), the number of paths to explore in the model ishigher. However, we observed that many of the paths in the model representthe same attack, applied on different elements of the model (for exampledropping different packets of time synchronization, or dropping such packetsat different runs of the system). Therefore, although a search query mayreturn hundreds of results, in most cases we only need to try one of them onthe code to test whether it applies, as they are all mostly equivalent. Thissignificantly reduces the number of attacks that need to be tested on thecode.Our results show that with a running time of a few hours, the modelchecker is able to analyze the model and find attacks on different executionpaths of the model. Since the analysis is done offline prior to deployment,we do not expect the analysis time to be a bottleneck. Further, our formal885.4. EvaluationAttacker action Time (h) Attacks FoundDropping packets 0.002 12Replay 0.005 845System rebooting 1.9 6452Table 5.2: Performance of model checker for different attacksmodel captures the design-level properties of smart meters, and not theirimplementation. Therefore, the size of the code does not affect the modelchecker’s performance.Another consideration in evaluating performance of the system is thetime taken to successfully map an attack found by the formal model to theimplementation. Based on our experience, this process was straightforwardand took a few minutes for each attack (maximum duration was half anhour). We also developed a semi-automated tool for this purpose (Sec.5.2.2). We acknowledge that we were very familiar with the SEGMeter’scode and implementation. Because we target the smart meter’s developersin our work, we expect them to be even more familiar with their code.Code analysisWe measure the time it takes to run the analysis on the transformed code.Table 5.3 shows the analysis time for three attacker actions: dropping mes-sages, replaying messages, and rebooting. The times shown in the table arerounded up to the nearest minute.We also show the number of points where the attacker actions are in-jected in the code. We find that the analysis time is correlated with thenumber of injection points. For example, the analysis time for droppingmessages action is only 4 minutes, as the number of injection locations issmall (6 locations in the code). The reason is that based on the model forthe action of dropping messages, it is only injected after http and serialcommunication API calls. However, the number of injected attacker actionsfor replaying messages and rebooting are far higher. The serial communi-cation may receive data asynchronously, therefore, the attacker may replay895.4. EvaluationAttacker action Analysis time (minutes) Number of injected actionsDropping messages 4 6Replaying messages 19 274Rebooting 23 327Table 5.3: Analysis timemessages at any time. Reboot action may occur at any time as well, hence,both these actions are injected after every instruction in the code.This increases the number of states of the code, and hence the analysistime increases to 19 minutes for replaying messages, and 23 minutes forrebooting.The reboot operation (as explained in Sec.5.4.4) jumps to the beginningof the code. This may increase the analysis time indefinitely. Therefore,we added a flag to limit the number of reboots by the symbolic executor toone. This is reasonable as a single reboot resets the run-time memory of thesystem and extra reboots will have similar effect. It is worth noting thatreboot operation is an extreme example of code transformation in terms ofincreasing the states of the code. Therefore, it is a measure of the worstcase time taken by our technique.The total analysis time for our technique for all attacker actions is lessthan an hour. This is acceptable as the analysis is performed offline, andprior to the deployment of the system.ComparisonThe total analysis time at the design-level is about 2 hours, which is twiceas long as code-level analysis. In our evaluation we observed that symbolicexecution engine (using its SMT solver) was able to drop many of executionpaths in the code that were not viable. Symbolic execution tries each execu-tion path only once, using symbolic values, which leads to shorter analysistime.905.4. Evaluation5.4.4 Comprehensiveness (RQ2.2)In this section, we first present the results of finding software-interferenceattacks for our design-level analysis technique and later, discuss the resultsof our code-level analysis technique with regard to RQ2.2.Design analysisOur formal model is based on an abstract model of smart meters. Hence,it does not factor in the implementation details of SEGMeter, and someattacks found by our model may not be applicable to it. This is because ourformal model must be applicable to other implementations of smart metersas well.In this RQ, we investigate which of the attacks found by the formalmodel are applicable to the SEGMeter. For each of the attacks, we attemptto execute the attack on SEGMeter, and check if it results in an unsafe stateon the meter. The results of this section show that the findings of the formalanalysis result in real attacks on the SEGMeterWe need additional hardware to mount some attacks. We explain the rea-sons later in this chapter. We use widely available inexpensive, off-the-shelfhardware, namely a USB-to-Serial cable and a relay timer, which togethercost less than $50 2. These do not require advanced skills to work with (e.g,soldering or working with laser beam), and hence the attacks are easy tomount.Rebooting meter An attacker may reboot and restart execution at anypoint by cutting off the power to the meter. Smart meters may or may nothave backup batter. Even if the meter has a backup battery, the attackermay disable it. As smart meters are deployed at homes and businesses, theymust have mechanisms (both at the implementation and the design level) tohandle these incidents without losing data. In our testbed, we observed thatthe system may reboot several times a day due to crashes. Therefore, losing2As of May 2016, from ebay.com915.4. Evaluationdata in such incidents is an indication of bugs in the system that attackersmay exploit.We study the effect of rebooting execution by adding its action model (asdefined in Sec.5.2.3), to the model of the smart meter. For this experiment,we define an unsafe state as one in which some of the consumption datais lost. In other words, state sB, reachable from state sA, is unsafe, if sAcontains some consumption data that is not included in sB. Here we considerthe states before data is submitted to the server. Below is an example ofthe search we perform on the model to find such unsafe states (simplifiedfor clarity):search sensor(N1,M1) sensor(N2,M2) sensor(N3,M3)⇒ sensor(N1,M1) sensor(N2,M2). (5.4)The above search phrase considers 3 sensor channels for the meter, repre-sented as sensor(Ni,Mi). Ni indicates the channel index, and Mi indicatesits corresponding measured energy. The search finds the paths where dataare received from three sensor channels, but only two of them have beenstored. This entails that the data measured by one of the sensor channels islost, and not sent to the server.Maude found 9 distinct groups of solutions for the cases where the systemmay face data loss as a result of system reboot. These solutions correspondto four meter components shown in Fig. 5.1, namely 1) receiving sensor data,2) storing sensor data to the flash, 3) retrieving data from flash memory,and 4) submitting data to the server. In our experiments, we observedthat in three of these components (1, 3, and 4), SEGMeter handles systemreboot correctly without losing data. However, we found that component2, namely storing data to flash memory, does not handle reboot correctly,and is vulnerable to attacks found by our model. In particular, storing datato flash memory lacks proper acknowledgment mechanisms which leads todata loss if the system is terminated at specific points in this component.We explain an example below.Example of system reboot attack on SEGMeter: To understand925.4. Evaluationthis attack, we need to understand how consumption data is updated inour smart meter model. Fig.5.13 shows the state diagram of this process.In state 1, the meter receives new data from sensors. These data may bedirectly sent to the server (state 2), or be stored in a data file. The mainreasons for storing data before sending them to the server are reduction ofcommunication overhead, and handling temporary unavailability of connec-tion to the server. When storing the data, the meter appends them to thepreviously stored data (states 3 and 4) and updates the data file (state 5).By letting the attacker reboot the system, our model produced paths fromstates 1, 3, and 4 of Fig.5.13, to the initial state of the system. In thesepaths, the meter receives new consumption data, but does not update thedata file, and hence the data is lost when the meter is rebooted.We explain the details of a reboot attack found on the meter, here. Weshow the snapshot of the code in SEGMeter associated with updating datafile in Fig.5.15. In line 2 (associated with state 3 of Fig.5.13), previouslyrecorded data (called all data) are read from the data file. In line 3 (asso-ciated with state 4 of Fig.5.13), current data and previous data are mergedtogether. In line 5 (associated with state 5 of Fig.5.13), the data file isupdated with the merged data.The meter updates the data file in alternating 30 second and 42 secondintervals. Smart meters follow a precise procedure for sampling data andcalculating consumption, to ensure correct billing. The indicated timingis the result of this process. We measured these by profiling the softwarerunning on the meter. Although software profiling may not be feasible foran adversary, we observed that data transmission via serial interface andstoring data, are indicated on SEGMeter by a flashing LED. Therefore, evensomeone able to observe the meter (access A1 in Table 5.1) may synchronizetheir operation of rebooting the meter with these time intervals.We used a programmable solid state timer (Fig. 5.14) to trigger thereboot, to ensure we can mount the attack at the precise time for maximumdamage. We placed the timer between the power source and the meter’spower adapter. We programmed the timer and repeatedly applied the rebootin 30 second and 42 second time intervals. We found that in 14 out of 20935.4. Evaluation1- Receive consumption data2-Send data to the server3-Fetch previous data4-Append new data to previous data5-Update the data fileTerminateStartFigure 5.13: The abstract model for updating sensor data file.tries, the new data is lost. However, we found that in 3 cases the attackshad even more devastating consequences. We observed that rebooting thesystem after line 4, not only erases new data, but in the worst case, all thepreviously stored data in the file are wiped out from the system. The reasonis that in line 4 of Fig. 5.15, the data file is opened in write mode (shownas ’w’ in the code), which erases the contents of the file. This is not aproblem in normal execution as the content of the file is read into memory(before overwriting it), and merged with the new data (line 3). However, ifwe reboot the system right after line 4, the meter does not get the chanceto write the in-memory data to the persistent storage. Rebooting the meterbefore the file has been closed results in losing a large portion of previouslystored data 3.Dropping messages One benefit of smart meters is that they enable theutility providers to adopt time-of-use billing. Therefore, smart meters peri-odically coordinate their clock with a time server, via time synchronizationmessages. In this attack, we were able to successfully compromise time syn-chronization for the SEGMeter by dropping time synchronization messages.An example of the search we perform in our model to find scenarios inwhich dropping time synchronization messages leads to an unsafe state isgiven timeSyncRequest ⇒ incorrectT ime. (5.5)3We found a similar vulnerability on YoMo [52], another open source smart meter,suggesting that this is a common design pattern.945.4. EvaluationFigure 5.14: We used a programmable solid state timer for rebooting thesystem at precise times, and a USB-to-Serial cable to mount replay attackon the meter.1.function update_node_list()// state 32. all_data = get_node_list()    …// state 43. all_data =      merge_tables(current_data,all_data)   …4. data_file = assert(, “w”))    …// state 55. for key, value in pairs(node_list) do…6.   data_file:write(data)7. end    …8. assert(data_file:close())    …9.endFigure 5.15: SEGMeter code for updating sensor data file. The commentsare added by us to show the mapping with the states in Fig. 5.13.The above search phrase explores the model to see if there are executionpaths that result in the meter having incorrect date or time settings, inspite of sending time synchronization messages to the server. This leads tothe consumption data having incorrect time stamps, which in turn leads toincorrect billing (with a time-of-use billing policy).Example of message-dropping attack on SEGMeter: Fig. 5.18shows the state diagram for time synchronization in the meter. In state2, the meter sends its current time to the server, and receives a responseindicating whether the current time is valid. If the time is valid, the metergoes to state 5, and starts the process of calculating and storing consumptiondata. Otherwise, it goes to state 3 where it sends a time adjustment request955.4. Evaluationto the server. The server responds with a command to adjust the time onthe meter (state 4), and the system checks whether the time adjustment wassuccessful (by going back to state 2). If not, the above process is repeateduntil it is successful.The attacker’s actions resulted in creating extra states (shown by dottedlines, as state 6) between states 3 and 4 of Fig. 5.18, where messages aredropped (eliminated). Dropping the messages results in the time value tobe invalid in our model (as no response is received from the server), andit does not transition to a state with valid time, which in turn results inincorrect time-labels for data.In our lab setup, we have root access to the machine that routes thesmart meter traffic to the campus gateway. This corresponds to access A3in Table 5.1, and is in line with our threat model in Sec. 1.4. On thatmachine, we added an IPTables rule that targets the packets destined forthe time server and drops them. We observed that this causes the smartmeter to get stuck in an infinite loop and hang. As a result, the meter isprevented from recording new consumption data. The details of this attackare presented below.1.function confirm_time_is_OK()2. while time_is_ok == false do    ...3.  time_is_ok = check_time()4.  if (time_is_ok == true) then 5.   set_time()6.   break7.  end8. end9.end(a) confirm time is ok()function1. function check_time()2.  output = call_seg_api()3.  if (output != nil) then4.   result = string.find(output, ''ok'')5.   if (search_result != nil) then6.    return true7.   end8.  end9.  return false10.end(b) check time() function1.function set_time()2. output = call_seg_api()3. if (output != nil) then4.  time = extract_time(output)    ...5.  local executable=''date -s''..time6.  os.execute(executable)    ...7. end8.end(c) set time() functionFigure 5.16: Time synchronization code for SEGMeter.Figures 5.16a, 5.16b, and 5.16c show the SEGMeter code for time syn-chronization. Function check time() (Fig.5.16b) corresponds to state 2 ofFig.5.18, and communicates with the server to verify whether the currenttime on the meter is correct. Function set time() (Fig.5.16c) corresponds tostate 4 of Fig.5.18 and requests a time from the server, and sets the meter’s965.4. Evaluation1.function serial_talker()// state 12.  serial_client = socket.connect()    …3.  while (status != “closed”) do     …// state 24.   command = “(all_nodes (start_data))”5.   serial_client:send(command .. “;\n”)     …// state 36.   status = serial_client:receive()     …7.  end    …// state 68.  serial_client:close()9.endFigure 5.17: SEGMeter code for communicating with the sensors on thesmart meter. The comments are added by us to show the mapping with thestates in Fig. 5.19.time to the server’s time. Function confirm time is ok() (Fig.5.16a) is themain function in charge of time synchronization. It calls check time() in line3 to verify whether the meter’s time is correct. If the time is incorrect, it willcall set time() (line 5). This process is repeated in a ’while’ loop until thetime is set correctly for the meter. The attacks found by our model corre-spond to dropping messages in line 2 in check time() or set time() functions.By dropping the time server responses, the boolean variable time is ok inconfirm time is ok() will remain false. This will cause the code to get stuckin an infinite loop and hang.Replaying messages In the smart meter, replaying a message involvestransitioning to a state prior to sending the message, which may cause thesystem to malfunction. Below is an example of a search we perform on ourmodel to check if replaying messages can lead to unsafe ask − for − sensor − data ⇒nullSocket N : sensorData. (5.6)In the above search, ask−for−sensor−data represents a state where adata-request command is received by the microcontroller. In an attack free975.4. Evaluation1-Start2-Check time with the server3-Ask the server for updated time4-Update time based on server’s response5-Check sensors for datatime is oktime is not ok6-Drop messagesFigure 5.18: The abstract model for time synchronization. The dotted linesare added by the attacker.execution, the microcontroller sends the newly calculated consumption data,and the other end (i.e., the gateway board) receives the data. In the query,we are checking whether it is possible that the microcontroller sends newsensor data, while the other end of the connection is closed (as indicated bynullSocket). This would result in the data being lost as it would be removedfrom the microcontroller’s memory after being sent, but not be recorded, asthere is no receiver on the other end.We found a successful instantiation of this attack on the SEGMeter thatwas identified by the formal model.Example of replaying message attack on SEGMeter: Fig. 5.19illustrates the state diagram of our model, when the microcontroller commu-nicates with the gateway board of the meter. In states 1 and 2, the gatewayboard establishes a connection with the microcontroller and sends a data-request command. In state 3, the data storage component listens for inputdata. If there is any data available, it reads them (state 4). Otherwise, theconnection times out (state 5). After all the data is received, or the datarequest times out, the connection is closed (state 6).A replay attack makes the system directly transition to states of themodel where a message is sent. In this case, such a transition representsjumping to state 2, as pointed to by a dashed arrow in Fig.5.19. Thisresults in creating a path from state 6 to state 2, and sending the data-985.4. Evaluationrequest message again after the connection is closed (in our model, socketwill transition to a null socket). Going through the data-request transitionwhile the state of the receiver socket is null in our model, results in the datanot transitioning to the received state, and later, to the stored state. Thisattack would result in data loss.We successfully mounted this attack on SEGMeter, using a laptop com-puter4 and a USB-to-Serial cable. As a result of this attack, we were ableto force the meter to delete the newly calculated data, without saving them.Note that we do not require root access to mount this attack, nor do weneed to decrypt any of the messages. Below we present the details of thisattack.Fig.5.17 shows a snapshot of the meter code associated with the statesshown in Fig.5.19. In line 2 of Fig.5.17, the communication unit of SEGMe-ter creates a socket to communicate with the microcontroller (correspondingto state 1 of Fig.5.19). In lines 4 and 5 of Fig.5.17, the communication unitprepares a data-request command and sends it to the sensors (correspondingto state 2 of Fig.5.19). This data-request command is a simple string and isnot encrypted. In line 6, the data storage component waits on the socket toreceive any incoming data (corresponding to state 3 of Fig.5.19). In the end,the communication unit closes the connection (line 8, corresponding to state6 of Fig.5.19). We observed that as a result of replaying data request com-mand, the microcontroller responds with the new sensor data and erases thedata from its memory. However, these data are not received by the gatewayboard as its connection is closed (line 8 of Fig.5.17) and consequently, willnot be recorded. This leads to incorrect billing to the attacker’s benefit.Summary: We observe that many of the attacks found by the modelchecker apply to the SEGMeter, and that they result in exposing non-trivialcorner cases and bugs in its implementation. Further, most attack can becarried out using inexpensive, off-the-shelf hardware components with littletechnical expertise on the part of the attacker.4The attack can be carried out through a specialized microcontroller such as an Aur-dino, and does not need a laptop.995.4. Evaluation1-Connect to sensors2-Send data request command3-Listen for input data4-Receive data5-Timeout6-Close the connectionStartAttacker actionFigure 5.19: The abstract model for sensor communicationCode analysisIn this section we explain the results of our code-level analysis technique forfinding software-interference attacks. As mentioned earlier, we consider 3 at-tacker actions, namely rebooting the system, dropping messages, and replay-ing messages. The functions defining these actions are shown in Fig. 5.20.The meter is uses 2 different APIs for communication. One is via LAN,using http, and the other is via serial interface. Therefore, we have two setsof actions targeting data received through each of these interfaces. Func-tion ’alt http receive’ targets http messages received via LAN, and function’alt serial receive()’ targets messages received via serial interface. Functions’alt http resend’ and ’alt serial resend()’ replay messages via LAN and serialinterface respectively. Function ’alt boot’ represents rebooting the system.It calls ’resetVariables’ function which reset all the variables in the codeto their initial values and then jumps to the beginning of the code. It isimportant to note that this way of representing reboot makes analysis viasymbolic execution easier as it provides a continuous execution flow.Our technique finds over 50 solutions that lead to software-interferenceattacks against the meter. Below we explain our results for each of theactions, and provide a detailed attack example found by our solution foreach category.Dropping messages We found 12 solutions where dropping messages,either communicated through LAN or serial interface, leads to an attackagainst the system. These solutions represent 3 different types of attacks.These attacks lead to 1) overflowing sensor buffer, 2) losing new consumption1005.4. Evaluationdata from sensors, and 3) getting stuck in the time-synchronization process.The first two attacks let the attacker pay less for electricity consumption.The third attack delays the meter which may affect recording of consumptiondata, and/or processing server commands. Below, we explain the first attackin more detail (please see the appendix for other examples).SEGMeter calculates consumption data based on sensor inputs. Thesedata are stored in a buffer in the sensor board. Periodically, the gatewayboard sends a data request message via serial interface to the sensor board,and receives consumption data stored in the buffer. Fig. 5.21 shows partof the code that generates consumption data and stores it in the buffer. Inlines 1 through 3 of Fig. 5.21, the buffer is represented as ’globalBuffer’and has the capacity of 350 characters. Function ’powerOutputHandler’calculates portion of electricity consumption (lines 5 to 13) data and addsthem to ’globalBuffer’ (line 14 onward). Dropping data request message tothe sensor board results in overflowing the buffer and losing consumptiondata. Our technique finds this attack as symbolic execution discovers a pathin which dropping messages leads to failure of the assertion that ensures theinput size added to the buffer, with respect to the buffer index, does notexceed the buffer capacity. We have provided the assertions we used in Table5.4 of the Appendix. The assertion violated here is the 4th assertion in row4 of Table 5.4.One approach to mitigate this problem would be to substitute pollingof data with a push mechanism to make sure that data is submitted to thegateway board. Also, the gateway board may respond with acknowledgmentmessages upon receiving data.Replaying messages We found 18 solutions where replaying messages re-sults in breaking security invariants in SEGMeter. These solutions indicatetwo different types of attacks. The first one results in losing new consump-tion data. The second group of solutions result in overflowing a data buffer.We explain an example of the second attack here in more detail (please seethe appendix for other examples).Fig. 5.22 shows the code snippet for ’serialHandler()’ function. The1015.4. Evaluationcontroller of the sensors calls this function when reading data via serialinterface. Received data will be stored in buffer, defined in line 2. Thelength of this buffer is set to 64, which is defined in line 2. This size is pickedbased on the maximum length of commands received by sensor controller. Inline 6, ’serialHandler’ loops over available characters on the serial interfaceand adds the characters to the buffer in line 12. As a precaution, in line9, ’serialHandler’ wraps around the buffer and starts over from index 0,if it goes over the size of the buffer. However, an attacker can exploitthis feature and send data of the size 64 - sizeof(command) to the sensorcontroller, after command string is sent to it. This leads to the controllerthinking the size of the received data (as indicated by length in the code)is 0, and therefore, ignoring the command. Our technique finds this attackas symbolic execution discovers a path in which replaying messages leads tofailure of an assertion that ensures that the command size is greater than 0.This assertion is presented in row 5 of Table 5.4.To mitigate this problem, the sensor controller may use two buffers forconsecutive communications, and alternate between them (i.e., dual buffer-ing). This ensures the content of the buffers are processed, before they areused again for receiving a message.Rebooting We found 23 solutions where rebooting may result in losingsensitive data in the system. These solutions represent 4 different attacks,as some solutions lead to the same results. These attacks lead to 1) los-ing previously calculated consumption data, 2) losing newly calculated con-sumption data, 3) missing server token used to identify the server, and 4)losing configuration data.The first two attacks allow the attacker to pay less for the consumedenergy. The third attack disrupts identification of the server. This leadsto meter mishandling server commands. The fourth attack affects correctcalculation and storage of data. Therefore, this attack may also lead topaying less for consumed data.We explain the third attack in more detail here (please see the appendixfor other examples). This attack may be mounted when the meter receives1025.4. Evaluationa new site token. This is a unique token that the meter may use to identifyitself to others. Periodically, the token changes and the meter receives a newtoken from the server. The process of receiving and storing a new token isshown in Fig. 5.23. Function ’seg talker’, in line 2, communicates with theserver and receives some data. This data may contain a new site token andis passed to ’process seg response’ function for processing. This functionexamines the response in line 3 and if contains a new site token, in line7, passes it to ’save site token’ to sore it in file. Since the meter does notstore state between line 2 of function ’seg talker’ and line 7 of function’save site token’, rebooting the meter at any point in this interval (and alsoduring execution of ’save site token’ itself) leads to losing the new site token.Our technique finds this attack as symbolic execution discovers a path inwhich rebooting leads to failure of an assertion that checks if the storedvalue of the token equals the latest value. This is the 4th assertion in row 1of Table 5.4.To mitigate this issue the meter must save its state during the process ofupdating site token. While starting up, it can read the state and continuefrom it, e.g., by requesting the new site token again.ComparisonAnalysis at the design level has false positives, as the analysis is done at anabstract level and some potential flaws are mitigated at the code level. Theattacks found via code analysis on the other hand, are a strict superset ofthe attacks found by design analysis, with no false positives.We note that design-level analysis is still helpful since it allows developersdiscover shortcomings of the design and avoid implementation mistakes thatmay lead to security attacks.5.4.5 Mounting the attacksTo evaluate feasibility of the attacks found by our analysis techniques, wemount them on SEGMeter. In our evaluation, our techniques found severalsolutions for each attack category.1035.4. EvaluationSecurity invariant Assertions- Check ’save data’ flag is set1- Data must be stored - Check ’seg data.dat’ file exists and is non-empty- Check ’node list.dat’ exists and is non-empty- Check ’site token’ has the latest value at startup2- Data must be sent to - Check ’talk to seg’ flag is set,communication board otherwise the communication fails3- Meter must meet - Check http timout is at most 5s,its functional otherwise delays operationsrequirements in a loop - Check loop counters do not exceed maximumlimit, otherwise delay operations- Check consecutive timestamps are within correct range4- Consumption data - Check consumption datamust be is within correct rangecalculated correctly - Check data size is smaller than sizeof buffer for storing data- Check buffer indices arewithin the range of buffer size- Check size of command buffers be5- Commands must be at least the size of command stringsreceived/processed correctly - Check the size ofcommands be greater than 0- Check buffer indices are within sthe range of buffer sizeTable 5.4: Assertions used for SEGMeterTo mount the solutions on the meter, we used commonly available hard-ware/software, and inexpensive tools to perform rebooting, replaying/droppingmessages.To drop and/or send messages to SEGMeter via serial interface, we useda 6-pin-serial-to-USB cable. This way we interfaced our laptop with themeter and intercepted the traffic. The parameters needed to be set for serialcommunication are data size in the frame (5-9 bits), stop bits (1-2 bits),parity bit (0-1 bit), and baud rate (there are about 10 common baud rates).There are a limited number of available configurations, and we found theconfiguration of 8bit data size, 1 stop bit, no parity and 38400 bps baudrate, work. The solutions indicate the exact points in run-time where theattacker actions must be applied. Having this information, we were ableto estimate the timing of messages indicated in the analysis solutions, viasoftware profiling. Based on the timing estimation, we were able to mountthe attacks targeting serial interface.To mount the attacks targeting http communication via LAN, we usedIPTables, which is a user-space firewall installed on many Linux distributions1045.5. Summaryby default. We selected one of the machines in our lab that route the trafficof SEGMeter, and inserted IPTables rules that drop the messages specifiedin our solution. We used source and destination IP addresses to identity themessages, and therefore, the attack was feasible regardless of encryption.To mount reboot attacks, we used a programmable solid state timer (Fig.5.14). This allows us to send reboot signals to at exact pre-programmedtimes. The solutions provide us with the exact execution points in the codewhere the reboot must be applied. Having this information, we identified thetiming of the reboot attacks via software profiling. Also, we took advantageof the LEDs on the meter that indicate the state of the meter (e.g., datacommunication via green flashes). We place the timer between the powersource and the meter. We let the timer repeatedly reboot the meter in thecalculated time intervals, and were able to successfully mount the attacksdiscussed in Sec. 5.4.4 and Sec. SummaryOne of the surprising results of this chapter is that we are able to surpassa high-level model based technique for discovering attacks both in termsof accuracy and scalability. Before we developed the code-level analysistechnique, we had expected it to be more accurate (i.e., have fewer false-positives), but slower than the design-level analysis. This was not the casehowever, even without considering the cost of translating in the model-basedtechnique, as our technique had fewer paths to analyze at the code level (asmany of the paths could be pruned as they were found to be infeasiblepaths). On the other hand, the design-level technique had to contend withlarger number of paths, as it could not easily determine which paths wereinfeasible. This seems to indicate that code-level techniques such as symbolicexecution may be more effective for security attack analysis than high-levelmodeling techniques.1055.5. Summaryfunction alt_http_receive(body, code, header, status)   return nil;endfunction alt_serial_receive(length)// returning nil for stream, status and partial   return nil, nil, nil;endfunction alt_http_resend(uri, method, msg, msg_len, content_type, response)n =“*n”)for i = 1, n do local body, code, headers, status =http.request{    url = uri,method = method,headers = {      ["content-length"] = message_length,      ["content-type"] = content_type},    source = ltn12.source.string(message),    sink = ltn12.sink.table(response)  }endreturn body, code, headers, statusendfunction alt_serial_resend(address, port, msg)serial_client = socket.connect(address, port)n =“*n”)   for i = 1, n doserial_client:send(msg)endserial_client:close()endfunction alt_boot()resetVariables()goto startendFigure 5.20: The functions defining dropping messages, replaying messages,and rebooting the system.1065.5. Summary1- #define BUFFER_SIZE 3502- char globalBuffer[BUFFER_SIZE]; 3- PString globalString(globalBuffer, sizeof (globalBuffer));4- void powerOutputHandler() { …5- for (int channel = 0; channel < CHANNELS; channel++) { 6- if (channel == 0 || channel == 1 || channel == 2) { 7- currentKW_1 += watts[channel];8- energySum_1 += energySum[channel];9- } else if (CHANNELS > 3) {                10- currentKW_2 += watts[channel];                11- energySum_2 += energySum[channel];            12- }        13- }            14- globalString += "(p_1 ";        15- globalString += currentKW_1;        16- globalString += ")";17- // Add energySum_1 , currentKW_2, energySum_2 to globalString…18- }Figure 5.21: Partial code that represents calculating parts of electricity con-sumption data and storing them in the buffer.1- void serialHandler(void) {2- static char buffer[64];3- int count = Serial.available();…4- if (count == 0) {…5- } else {6- for (byte index = 0; index < count; index++) {7- char ch =;8- if (length >= (sizeof (buffer) / sizeof (*buffer))) {9- length = 0;10- } else if (ch == '\n' || ch == ';') {…11- } else {12- buffer[length++] = ch;13- }14- }15- }       …16- }Figure 5.22: Code snippet for reading data from the serial interface.1075.5. Summary1- function seg_talker(sexp) ...2- local this_response = call_seg_api(this_resource, "PUT", sexp)  3- if (this_response ~= nil) then    4- talker_win = process_seg_response(this_response)  5- else    ...6- end... 7- end1- function process_seg_response(response)  ...2- if (response ~= nil and response ~= "") then    3- if (response:sub(1, 7) == "(site= ") then      4- local start, finish = response:find("\n", 1, PLAIN)      5- local message = response:sub(1, start - 1)      6- response = response:sub(finish + 1)      7- save_site_token(message:sub(8, -2))    8- end... 9- end...10- endFigure 5.23: Code snippet representing receiving and storing site token.108Chapter 6Conclusion and Future Work6.1 ConclusionIn light of massive expansion of modern networked embedded devices, andgrowing attacks against them, the main goal of this thesis was to developtechniques to make them more secure. To achieve this goal, we laid outtwo problems and proposed techniques to address them. The first problemwas developing host-based intrusion detection systems (IDS) for embeddeddevices, given their limited resources. Following defense-in-depth best prac-tices, we defined the second problem as analyzing the security of the softwarerunning on the embedded device against attacks. This allows the developersto improve the security, given that other defense layers such as IDS mayhave false negatives.We discussed the first problem in Chapters 3 and 4. In Chapter 3, weidentified the constraints posed by smart meters for IDSes, and designeda model-based IDS that satisfies these constraints. We showed that ourIDS incurs low performance overhead on our smart meter while providingreasonable detection coverage for both known and unknown attacks. InChapter 4, we formulated the problem of building IDS for embedded systemsas an optimization problem. Given the memory constraints of the device, theset of security properties and the invariants of the system verifying thoseproperties, we build an IDS within the memory constraints of the devicethat maximizes the coverage for the security properties. Our technique isflexible in terms of accommodating user-defined coverage functions. Wealso defined two coverage functions and built two IDSes based on them:MaxMinCoverage IDS and MaxProperty IDS. We showed that using 4MBof memory, MaxMinCoverage IDS is able to detect 80% of attacks against1096.1. Conclusionthe security properties of the system. Also, MaxProperty IDS is able toprovide 100% detection rate for 5 (out of 10) of the security properties ofthe system. Furthermore, our IDSes incur low performance overhead ofless than 7% on the system, and the detection results of our IDSes complywith their estimated coverage at design time, even under severe memoryconstraints. We further extended the initial IDS-generation algorithm. Weshowed by running a pre-processor algorithm we may reduce the size ofthe invariants and improve the coverage of the IDS by over 30%. Also, byadding a ranking relationship between the invariants, we were able to assigna larger share of memory to important invariants and improve the coverageof important components by up to 100%.We discussed the second problem in Chapter 5. We proposed two tech-niques to analyze security of embedded devices. This first technique an-alyzes the design of embedded systems. It helps developers identify theshortcomings of the design and address them during implementation. Thisis important as accounting for design/implementation flaws at early stagesof software development reduces the cost. This of course does not guaranteethat developers do not make mistakes and introduce security bugs at the im-plementation phase. Therefore, we proposed another technique to analyzesthe implementation as well. We used smart meters, a widely-used modernembedded device, as a testbed. To analyze the design of smart meters, webuild a formal model of their design specifications using rewriting logic. Wealso formally define a set of attacker actions, and use model-checking to findall the possible sequences of the attacker actions that may transition thesystem to an unsafe state. Using the formal model, we were able to findattacks within a modest time of about two hours on the meter. We success-fully mapped a sizable number of the attacks found on the design-level, toan implementation of smart meters, namely SEGMeter. Furthermore, wedeveloped a technique to analyze the security at the code-level as well. Ourtechnique uses a combination of code injection and symbolic execution tofind attacks that violate security assertions in the code. We evaluated ourtechnique on SEGMeter and it was able to find 9 different types of attacks,and over 50 ways to mount them. We successfully carried out those attacks1106.2. Expected impactusing commodity, inexpensive hardware that is easy to use, thereby demon-strating their practicality. Further, our technique completed the analysis inless than an hour in total, which is acceptable as the analysis is done offline.6.2 Expected impactThe first impact of this work is providing insights regarding overcomingresource limitation of embedded devices, for security developers. Many se-curity mechanisms rely on a model for the correct behavior of the systemthey are monitoring. This model may be large and verifying it in real-timerequires processing resources. Our research shows that even a partial model,that requires significantly less resources than the complete model, may pro-vide comparable security coverage. In other words, approximate securitysolutions are effective for modern embedded system and provide high cover-age while requiring significantly less resources. As demonstrated in Chapter4, extracting such partial models may be achieved via automated algorithmsand static analysis techniques. This implies that such techniques may be in-tegrated with IDEs and tools for developing embedded software and hence,make building security solutions that meet the system’s limitations, moreconvenient.Furthermore, our research shows that the design specifications for em-bedded devices, e.g., smart meters, that are deployed in large scale, leaveroom for implementation flaws with high security impact that could other-wise be mitigated. Each class of embedded systems share significant similar-ities in use cases and architecture. Therefore, given our approach in Chapter5 to analyze the design of such systems, utility providers and device manu-facturers may provide security guidelines to improve implementation efforts.For instance, such guidelines may include defining standards for data storageand communication between components of the system.1116.3. Limitations6.3 LimitationsIn this section, we discuss aspects of our thesis that may limit its impactand demand further studies.Generalizability: In this thesis, we focused on smart meters as a casestudy. Although we expect the same ideas be extensible to other classes ofembedded devices, more research/evaluation on other platforms are neces-sary. The main requirement for applying our techniques for building IDSand performing security analysis on other systems are 1) developing the setof security invariants for the target class of embedded systems, and 2) iden-tifying the viable attacker actions specific to those systems. For example,AUTOSAR (AUTomotive Open System ARchitecture) is an open softwarearchitecture that provides the basic infrastructure for developing vehicularsoftware. Similar platforms have been proposed for other classes of embed-ded systems, e.g., medical devices [1, 4]. Given the open and standardizedarchitecture of these systems, we believe we should be able to take a similarapproach for them. Extending our work to these platforms would be aninteresting future direction.Scalability: We use symbolic execution to analyze the security of soft-ware running on embedded devices, along with an attacker model. Theefficiency of symbolic execution depends on the structure and size of code.Increasing the number of attacker actions and their complexity, results in amore complex code with larger state space. This increases the time taken tofind attacks. Also, potential parallelism in the software poses the challengeof state intra-dependencies. This suggests that further research is needed, tostudy the scalability of our analysis technique when applied to a wider rangeof attacker actions and more complex code. Intuitively, we do not expectthe software running on embedded systems to have high complexity as theyare normally running on devices with limited computational and memoryresources. Also, there exist techniques to improve scalability of symbolicexecution when applied to larger code. These include combining concreteand symbolic values [37], and trade-offs between precision and scalability[19]. Moreover, there are research efforts to address scalability of symbolic1126.4. Future workexecutions to parallel applications as well [17, 72, 73]. We expect to be ableto leverage these techniques to make our solution more scalable.Reliance on invariants: When building an IDS, we rely on a setof abstract security invariants that are provided by security experts, andgenerated based on the specifications of the system. Applying our techniqueon a new class of devices requires development of a new set of abstractinvariants. This is a manual process. However, there are research efforts indeveloping tools, e.g., InvGen [39], that automate the process of generatinginvariants. We expect such efforts, eventually, enable us to minimize thenumber of manual steps required in our technique for building IDSes.System calls: Our IDS monitors system call traces of the softwarerunning on the embedded device to check correctness of software behavior.Intercepting system calls made by software does not require source codemodification and may be done using tools such as strace. However, em-bedded devices may have customized software stack. Therefore, they maybe developed to use a simplified OS or even use no OS at all. Our tech-nique is able to accommodate any input trace, other than system calls, fromthe software as well. However, further research is required to opt for suit-able substitute traces, and to produce them at run time. Instrumentingthe code for generating logs of critical operations of the system may be aviable approach to address this issue. However, it is important that codeinstrumentation does not affect real-time properties of the software.6.4 Future workOther constraints: In this thesis, we focused on memory, as the primaryconstraint for deployment of host-based security mechanisms for embeddedsystems. However, the limitations these systems impose on developers maygo beyond that. Energy and CPU are instances of resources that can makedevelopment of security mechanisms challenging. Many embedded devices,such as implantable medical devices, are battery-powered. These devicesmust devote most of their available energy to executing the main tasks theyare designed to carry out. This leaves small room for running and external1136.4. Future workapplication such as an IDS. Furthermore, these systems are manufactured tobe cost-effective and are generally equipped with CPU that is only sufficientfor the application they are running. Even if the next-generation devicesare equipped with faster processors, there are already millions of deployedembedded systems, updating which is infeasible. This makes monitoringthese systems, especially when real-time monitoring is required, challenging.Extending our technique for building real-time security mechanisms thataccount for CPU and energy constraints is an interesting direction.Concurrent programs: In our security analysis technique presented inChapter 5, we assume that the program we are analyzing is single-threaded,as most symbolic execution techniques work only for single threaded pro-grams. Extending this approach to concurrent programs increases the us-ability of our technique. There are efforts for developing symbolic executiontechniques for multi-threaded programs e.g., Bergan et. al. [14] which po-tentially facilitate analysis of concurrent programs as well. However, execu-tion scenarios for concurrent programs may increase exponentially and thismay significantly downgrade analysis performance. Measuring the impactof concurrent programs on efficiency of our technique and addressing it, isanother future research direction.Tools for secure development of modern embedded systemsWhile modern embedded devices run Operating Systems and applicationson top of their specialized hardware, their software stack may completely dif-fer from standard OSes such as Android, iOS, and common distributions ofLinux. This essentially means that standard enterprise analysis tools won’tbe applicable to them. On the other hand, manufacturers are rushing to addnetwork-connectivity to their devices and enable the newest features at low-est cost. These lead to overlooking complications of software and hardwaresecurity and finally vulnerability of the embedded systems. In light of this,building standard security tools that integrate with design/implementationlife-cycle of modern embedded systems is an important future work. Thesetools must facilitate 1) development of threat model, 2) integration of threatmodel with code, and 3) management of the system after deployment:1146.4. Future work• As discussed in Chapter 5, the attacker model for embedded systems,unlike remote servers, may have unique capabilities. These capabil-ities may be the result of proximity, physical access, etc. We calledthe attacks resulting from such capabilities, software-interference at-tacks. We manually defined code snippets for select such capabilities.However, developing general tools to create the attacker model for dif-ferent classes of embedded systems and creating formal model for themis an important step to integrate security with development life-cycleof embedded systems.• Development tools for embedded systems must have the capability ofintegrating with the system’s threat model. Such integration in thedevelopment environment allows for conveniently analyzing and cor-recting the code at the development phase. This is challenging asthreats must be specified formally, be translated to various program-ming languages, and be integrated with the code.• Eventually, vulnerabilities will be discovered in embedded devices afterthey have been shipped. Therefore, these systems must be managedremotely. It is imperative to develop security management tools thatprovide Over-The-Air updating functionalities, and control configura-tion of host-based security technologies. This is challenging as themanagement tools must account for constraints of embedded systemssuch as battery and bandwidth limitations. Without such functionali-ties, discovered vulnerabilities will persist in the embedded devices forextended time periods.Developing tools that address the above aspects and integrate with develop-ment life-cycle of embedded devices facilitates secure-development of thesesystems.Using security analysis technique for optimizing IDS: Techniquesproposed in chapter 5 for analyzing security of embedded systems via findingattacks against them, may be used as an evaluation mechanism for IDSes,e.g., the one proposed in chapter 4. Leveraging this evaluation method may1156.5. Final wordsallow us to improve the coverage of IDS. Consequently, we may be able tooptimize the IDS with respect to a specific attacker, by iterating throughthis evaluation cycle. Exploring this would be an interesting direction.6.5 Final wordsAs embedded devices become more popular and are deployed in homes, busi-nesses, and for personal use, the security challenges they pose will increaseas well. Given the rapid growth in the number of in-use embedded devices,vulnerable systems not only impact local owners, they can also be used asbots and perform large scale DDoS attacks.In this thesis, we explored two host-based measures to improve security ofembedded devices. However, there is need to develop security measures thatcover all aspects of design, implementation, administration, and usabilityof these systems. The latter is especially important as the end-users ofthese systems may have limited understanding of device’s operations andhence, may not follow best security practices for using them. Therefore,it is imperative to invest in research for security of embedded devices, toeffectively address this pressing problem.116Bibliography[1] Green Hills medical devices platform. last accessed: July 31 2017).[2] Information and Technology Standards, Advanced Me-tering Infrastructure, Government of Ontario Canada. (Date lastaccessed: July 31 2017).[3] UK Department of Energy, smart meter design document. (Date last accessed: July 312017).[4] Wind River medical devices platform. (Date last accessed:July 31 2017).[5] Cert research anual report, 2009.[6] Mart´ın Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Control-flow integrity. In Proceedings of the 12th ACM conference on Computerand communications security, pages 340–353. ACM, 2005.[7] Pandya V. Acharya S. International Journal of Electronics and Com-puter Science Engineering (IJECSE), 2013.[8] Acunetix web application security scanner. (Date last accessed: July 31 2017).117Bibliography[9] Jean Arlat, Alain Costes, Yves Crouzet, Jean-Claude Laprie, and DavidPowell. Fault injection and dependability evaluation of fault-tolerantsystems. IEEE Transactions on Computers, pages 913–923, 1993.[10] Christel Baier, Joost-Pieter Katoen, et al. Principles of model checking,volume 26202649. MIT press Cambridge, 2008.[11] David Basin, Felix Klaedtke, and Samuel Mller. Policy monitoringin first-order temporal logic. In Computer Aided Verification, volume6174 of Lecture Notes in Computer Science, pages 1–18. Springer BerlinHeidelberg, 2010.[12] Arduino home page. (Date last accessed: July31 2017).[13] John E. Bentley, Wachovia Bank, and Charlotte NC. Software testingfundamentals-concepts, roles, and terminology. Technical report, SASInstitute, 01 2008.[14] Tom Bergan, Dan Grossman, and Luis Ceze. Symbolic execution ofmultithreaded programs from arbitrary program contexts. ACM SIG-PLAN Notices, 49(10):491–506, 2014.[15] R. Berthier, W.H. Sanders, and H. Khurana. Intrusion detection foradvanced metering infrastructures: Requirements and architecture di-rections. In Smart Grid Communications, pages 350 – 355, 2010.[16] Robin Berthier and William H. Sanders. Specification-based intrusiondetection for advanced metering infrastructures. PRDC, IEEE, 0, 2011.[17] Stefan Bucur, Vlad Ureche, Cristian Zamfir, and George Candea. Par-allel symbolic execution for automated real-world software testing. InProceedings of the sixth conference on Computer systems, pages 183–198. ACM, 2011.[18] Eric J Byres, Matthew Franz, and Darrin Miller. The use of attacktrees in assessing vulnerabilities in scada systems. In Proceedings of theInternational Infrastructure Survivability Workshop. Citeseer, 2004.118Bibliography[19] Cristian Cadar and Koushik Sen. Symbolic execution for software test-ing: three decades later. Communications of the ACM, 56(2):82–90,2013.[20] Joao Carreira, Henrique Madeira, Joa˜o Gabriel Silva, et al. Xcep-tion: Software fault injection and monitoring in processor functionalunits. Dependable Computing and Fault Tolerant Systems, pages 245–266, 1998.[21] Shuo Chen, Jun Xu, Nithin Nakka, Zbigniew Kalbarczyk, and Ravis-hankar K Iyer. Defeating memory corruption attacks via pointer taint-edness detection. In DSN 2005., pages 378–387. IEEE, 2005.[22] Yuqun Chen, Ramarathnam Venkatesan, Matthew Cary, RuomingPang, Saurabh Sinha, and Mariusz H Jakubowski. Oblivious hash-ing: A stealthy software integrity verification primitive. Work, pages400–414, 2003.[23] Clang: a C language family frontend for LLVM. (Date last accessed: July 31 2017).[24] Manuel Clavel, Francisco Dura´n, Steven Eker, Patrick Lincoln, NarcisoMart´ı-Oliet, Jose´ Meseguer, and Carolyn Talcott. All about maude-ahigh-performance logical framework: how to specify, program and verifysystems in rewriting logic. Springer-Verlag, 2007.[25] Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, PatrickVenter, Daniel Weil, and Sergio Yovine. Taxys: A tool for the devel-opment and verification of real-time embedded systems? In ComputerAided Verification, pages 391–395. Springer, 2001.[26] Common Vulnerabilities and Exposures. last accessed: July 31 2017).[27] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. InInternational conference on Tools and Algorithms for the Constructionand Analysis of Systems, pages 337–340. Springer, 2008.119Bibliography[28] Department of Energy and Climate Change and the Office ofGas and Electricity Markets. Smart metering response toprospectus consultation, March 2011.[29] E Allen Emerson. Temporal and modal logic. Handbook of Theoret-ical Computer Science, Volume B: Formal Models and Sematics (B),995:1072, 1990.[30] Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant,Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. The daikonsystem for dynamic detection of likely invariants. Science of ComputerProgramming, 69(1):35–45, 2007.[31] Eleazar Eskin, Salvatore J. Stolfo, and Wenke Lee. Modeling systemcalls for intrusion detection with dynamic window sizes. DARPA In-formation Survivability Conference and Exposition,, 1:0165, 2001.[32] FBI: Smart Meter Hacks Likely to Spread. (Datelast accessed: July 31 2017).[33] Eduardo Fernandez, Juan Pelaez, and Maria Larrondo-Petrie. Attackpatterns: A new forensic and design tool. In Advances in digital foren-sics III, pages 345–357. Springer, 2007.[34] Paul Gastin and Denis Oddoux. Fast LTL to Bu¨chi automata trans-lation. In Proceedings of CAV’01, volume 2102 of Lecture Notes inComputer Science, Paris, France, July 2001. Springer.[35] Michael Gegick and Laurie Williams. Matching attack patterns to se-curity vulnerabilities in software-intensive system designs. ACM SIG-SOFT Software Engineering Notes, 30(4):1–7, 2005.120Bibliography[36] Jonathon T. Giffin, Somesh Jha, and Barton P. Miller. Efficient context-sensitive intrusion detection. In Proceedings of the 11th NDSS Sympo-sium, 2004.[37] Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: directedautomated random testing. In ACM Sigplan Notices, volume 40, pages213–223. ACM, 2005.[38] Hendra Gunadi and Alwen Tiu. Efficient runtime monitoring with met-ric temporal logic: A case study in the android operating system. InFM 2014: Formal Methods, volume 8442 of Lecture Notes in ComputerScience. Springer International Publishing, 2014.[39] Ashutosh Gupta and Andrey Rybalchenko. Invgen: An efficient in-variant generator. In Computer Aided Verification, pages 634–640.Springer, 2009.[40] Simon Hansman and Ray Hunt. A taxonomy of network and computerattacks. Computers & Security, 24(1):31 – 43, 2005.[41] Xuan Dau Hoang, Jiankun Hu, and Peter Bertok. A multi-layer modelfor anomaly intrusion detection using program sequences of systemcalls. In Proc. 11th IEEE Intl. Conference on Networks, 2003.[42] HP WebInspect. (Date last ac-cessed: July 31 2017).[43] Jiankun Hu, Xinghuo Yu, D. Qiu, and Hsiao-Hwa Chen. A simple andefficient hidden markov model scheme for host- based anomaly intrusiondetection. Netwrk. Mag. of Global Internetwkg., 23(1):42–47, January2009.[44] Wenjie Hu. Robust support vector machines for anomaly detection. InIn Proc. ICMLA03, 2003.[45] IBM Security AppScan. (Date last accessed: July 31 2017).121Bibliography[46] 1016-1998-IEEE Recommended Practice for Software Design De-scriptions. (Date last accessed: July 31 2017).[47] In-Stat and NDP Group Company. (Date last accessed: July 31 2017).[48] Hacking Medical Devices for Fun and Insulin: Breaking theHuman. (Date last ac-cessed: July 31 2017).[49] Somesh Jha, Oleg Sheyner, and Jeannette Wing. Two formal analysesof attack graphs. In Computer Security Foundations Workshop, 2002.Proceedings. 15th IEEE, pages 49–63. IEEE, 2002.[50] Hacking Humans. last accessed: July 31 2017).[51] Himanshu Khurana, Mark Hadley, Ning Lu, and Deborah A. Frincke.Smart-grid security issues. IEEE Security & Privacy, pages 81–85, 2010.[52] Christoph Klemenjak, Dominik Egarter, and Wilfried Elmenreich.Yomo: the arduino-based smart metering board. Computer Science-Research and Development, pages 1–7, 2015.[53] Ricardo Koller, Raju Rangaswami, Joseph Marrero, Igor Hernandez,Geoffrey Smith, Mandy Barsilai, Silviu Necula, S. Masoud Sadjadi,Tao Li, and Krista Merrill. Anatomy of a real-time intrusion preventionsystem. In ICAX, ICAC ’08, pages 151–160, Washington, DC, USA,2008. IEEE Computer Society.[54] Karl Koscher, Alexei Czeskis, Franziska Roesner, Shwetak Patel, Ta-dayoshi Kohno, Stephen Checkoway, Damon McCoy, Brian Kantor,Danny Anderson, Hovav Shacham, and Stefan Savage. Experimen-tal security analysis of a modern automobile. In Proceedings of the122Bibliography2010 IEEE Symposium on Security and Privacy, SP ’10, pages 447–462, Washington, DC, USA, 2010. IEEE Computer Society.[55] Michael LeMay, George Gross, Carl A. Gunter, and Sanjam Garg. Uni-fied architecture for large-scale attested metering. In Proceedings ofHICCS’07, Washington, DC, USA, 2007. IEEE Computer Society.[56] N. Lewson. Smart meter crypto flaw worse thanthought, 2010. (Date last ac-cessed: July 31 2017).[57] FabrizioMaria Maggi, Marco Montali, Michael Westergaard, andWilM.P. van der Aalst. Monitoring business constraints with lineartemporal logic: An approach based on colored automata. In BusinessProcess Management, volume 6896 of Lecture Notes in Computer Sci-ence, pages 132–147. Springer Berlin Heidelberg, 2011.[58] FabrizioMaria Maggi, Michael Westergaard, Marco Montali, andWilM.P. van der Aalst. Runtime verification of ltl-based declarativeprocess models. In Runtime Verification, volume 7186 of Lecture Notesin Computer Science, pages 131–146. Springer Berlin Heidelberg, 2012.[59] Narciso Mart´ı-Oliet and Jose´ Meseguer. Rewriting logic as a logicaland semantic framework. Electronic Notes in Theoretical ComputerScience, 4:190–225, 1996.[60] Stephen McLaughlin, Dmitry Podkuiko, Sergei Miadzvezhanka, AdamDelozier, and Patrick McDaniel. Multi-vendor penetration testing inthe advanced metering infrastructure. In Proceedings of ACSAC’10,pages 107–116. ACM, 2010.[61] Barton P Miller, Louis Fredriksen, and Bryan So. An empirical study ofthe reliability of unix utilities. Communications of the ACM, 33(12):32–44, 1990.123Bibliography[62] Yilin Mo, Tiffany Hyun-Jin Kim, Kenneth Brancik, Dona Dickinson,Heejo Lee, Adrian Perrig, and Bruno Sinopoli. Cyber–physical securityof a smart grid infrastructure. Proceedings of the IEEE, 100(1):195–209,2012.[63] Sibin Mohan, Jaesik Choi, Man-Ki Yoon, Lui Sha, and Jung-Eun Kim.Securecore: A multicore-based intrusion detection architecture for real-time embedded systems. In Proceedings of the 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS),Washington, DC, USA, 2013. IEEE Computer Society.[64] Mehdi Moradi and Mohammad Zulkernine. A neural network based sys-tem for intrusion detection and classification of attacks. In Proceedingsof the 2004 IEEE international conference on advances in intelligentsystems-theory and applications, 2004.[65] Anderson Morais, Eliane Martins, Ana Cavalli, and Willy Jimenez.Security protocol testing using attack trees. In Computational Scienceand Engineering, 2009. CSE’09. International Conference on, volume 2,pages 690–697. IEEE, 2009.[66] National Vulnerability Database. (Date lastaccessed: July 31 2017).[67] Nuno Neves, Joao Antunes, Miguel Correia, Paulo Verissimo, and RuiNeves. Using attack injection to discover new vulnerabilities. In De-pendable Systems and Networks, 2006. DSN 2006. International Con-ference on, pages 457–466. IEEE, 2006.[68] James Newsome and Dawn Song. Dynamic taint analysis: Automaticdetection, analysis, and signature generation of exploit attacks on com-modity software. In In In Proceedings of the 12th Network and Dis-tributed Systems Security Symposium. Citeseer, 2005.[69] Computer Security Division Information Technology Laboratory Na-tional Institute of Standards and Technology. Performance measure-124Bibliographyment guide for information security. NIST Special Publication 800-55Revision 1, 2008.[70] Ahmed Patel, Qais Qassim, and Christopher Wills. A survey of in-trusion detection and prevention systems. Information ManagementComputer Security, 18(4).[71] M. McEvilley R. Ross, J.C. Oren. Systems security engineeringl anintegrated approach to building trustworthy resilient systems. NISTSpecial Publication 800-160, May 2014.[72] Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin LucienKaminski, Klaus Wehrle, Carsten Weise, and Stefan Kowalewski. Scal-able symbolic execution of distributed systems. In Distributed Comput-ing Systems (ICDCS), 2011 31st International Conference on, pages333–342. IEEE, 2011.[73] Raimondas Sasnauskas, Jo´ A´gila Bitsch Link, Muhammad Hamad Al-izai, and Klaus Wehrle. Kleenet: automatic bug hunting in sensornetwork applications. In Proceedings of the 6th ACM conference onEmbedded network sensor systems, pages 425–426. ACM, 2008.[74] Dries Schellekens, Brecht Wyseur, and Bart Preneel. Remote attesta-tion on legacy operating systems with trusted platform modules. Sci.Comput. Program., 74:13–22, December 2008.[75] Arvind Seshadri, Mark Luk, Elaine Shi, Adrian Perrig, Leendert vanDoorn, and Pradeep Khosla. Pioneer: verifying code integrity and en-forcing untampered code execution on legacy systems. In Proceedings ofthe twentieth ACM symposium on Operating systems principles, SOSP’05, pages 1–16, New York, NY, USA, 2005. ACM.[76] Oleg Sheyner, Joshua Haines, Somesh Jha, Richard Lippmann, andJeannette M Wing. Automated generation and analysis of attackgraphs. In Security and privacy, 2002. Proceedings. 2002 IEEE Sym-posium on, pages 273–284. IEEE, 2002.125Bibliography[77] Smart Energy Groups Home Page. last accessed: July 31 2017).[78] David T Stott, Benjamin Floering, Daniel Burke, Zbigniew Kalbarczpk,and Ravishankar K Iyer. Nftape: a framework for assessing depend-ability in distributed systems with lightweight fault injectors. In IPDS2000., pages 91–100. IEEE, 2000.[79] SymbolicLua. (Datelast accessed: July 31 2017).[80] Olivier Thonnard and Marc Dacier. A framework for attack patterns’discovery in honeynet data. digital investigation, 5:S128–S139, 2008.[81] Kuan-Yu Tseng, Daniel Chen, Zbigniew Kalbarczyk, and Ravis-hankar K Iyer. Characterization of the error resiliency of power grid sub-station devices. In Dependable Systems and Networks (DSN), 2012 42ndAnnual IEEE/IFIP International Conference on, pages 1–8. IEEE,2012.[82] Ahmed U and Masood A. Host based intrusion detection using rbfneural networks. In In Proc. International Conference on EmergingTechnologies., 2009.[83] David Wagner and Drew Dean. Intrusion detection via static analysis.In Proceedings S&P’01, USA, 2001. IEEE Computer Society.[84] Christina Warrender, Stephanie Forrest, and Barak Pearlmutter. De-tecting intrusions using system calls: Alternative data models. In InIEEE S&P’99. IEEE Computer Society, 1999.[85] Pierre Wolper. Temporal logic can be more expressive. Informationand control, 56(1):72–99, 1983.[86] Nong Ye, Syed Masum Emran, Qiang Chen, and Sean Vilbert. Mul-tivariate statistical analysis of audit trails for host-based intrusion de-tection. IEEE Trans. Comput., 51(7):810–820, July 2002.126Bibliography[87] K. Zetter. Security pros question deployment of smart meters. ThreatLevel: Privacy, Crime and Security Online, March 2010.127


Citation Scheme:


Citations by CSL (citeproc-js)

Usage Statistics



Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            async >
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:


Related Items