Networking and Security Research Center
Contents
1. if M H uo then if IncMapping 4 U po spec Vm Ho Var M then 8 return T 1 2 3 4 h Pop spec 5 6 7 9 return L We use the NuSMV model checker 11 for deciding M pu The running time of IncMapping is dependent on the number of false positive mappings for each specification in the specification bounded below by 2 speci fication and above by O Vii 3 3 2 Unambiguous Specifications Consider the problem of writing a specification for the chemical mixer process shown in Figure 1 First one must define the names in Vg Denoting input variable names with an let Ij 13 and 13 be the names of the low mid and high level switches respectively and let start be the start button Additionally let va and vg be the valves for ingredients A and B mixer be the mixer and va be the drainage valve As in the figure Vm 21 2 3 4 U y1 Y2 Y3 Ya Recall the specification sbutton from above While sbutton is an accurate specification of plant behavior it is also ambiguous To see this we first consider the case of the correct true positive mapping urp start gt x4 va gt yi When the map ping is applied to the CTL specification we get urp sbutton INIT z4 v4 gt AX y urr is the correct mapping because 1 trp sbutton holds under the control logic Figure 1 c and 2 xa and y are the names of the control input and output for the devices that the2. behavior an adver Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page To copy otherwise to republish to post on servers or to redistribute to lists requires prior specific permission and or a fee Copyright 200X ACM X XXXXX XX X XX XX 10 00 Patrick McDaniel Systems and Internet Infrastructure Laboratory Pennsylvania State Univesity mcdaniel cse psu edu sary cannot construct a payload for specific devices without know ing how the PLC interfaces with those devices However there is often no way of determining which PLC memory locations regulate which devices This paper presents SABOT Specification based Attacks on Boolean Operations and Timers a proof of concept attack tool for gen erating PLC payloads based on an adversary provided specifica tion of device behavior in the target control system SABOT s main purpose is to recover semantics of PLC memory locations that are mapped to physical devices Specifically SABOT determines which memory locations map to the devices in a behavioral specification of the target plant This enables an adversary with a goal to attack specific devices to automatically instantiate that attack for a spe cific PLC in the victim control system Unlike previous att
3. for valve B y2 is activated immediately when y L on the condition x2 T y2 then remains ON until the draining process begins with ya The mixer y3 is on as long as the level in the tank has reached midway and has not sub sequently been emptied Finally the drain ya is activated when the tank is full and remains ON until the tank is empty A logic program must be compiled to a PLC s native instruction set architecture ISA before being uploaded to the PLC While ISAs vary between PLC vendors many are equivalent to the IEC 61131 3 standard for the Instruction List IL programming lan guage 25 We implement an IL decompiler in Section 3 2 T4 y2 Start 010 24304 X T3 Y Fill A p72 PLC Hf Y Mix B Y3 yy2yYzya V Y DK ys UY Vm Drain Product a z T2 T4 y Y2 Y3 Ya Process Control Logic High Level Low Level Switch i Fill A EaR S Get EI E High Level Switc Add B Start Button Y2 aA Y4 eas Mix I lient A V ngred is alve yy eV ys Az Ingredient B Valve Drai rain Mixer ie VNR Drain Valve b c Figure 1 An example plant and process specification for a chemical mixing control process 2 2 Attacking PLCs Control systems have shown to be vulnerable to attacks through sensors 36 human machine interfaces 2 and PLCs 18 6 40 In this work we focus on the last of these due to the complet
4. further a typical 4 way traffic light with red yellow1 and green in the North South direction and redz yellow2z and greenz in the East West direction Ignoring inputs from pedestrians or road sensors the traffic light follows the circular timed sequence red redz redi1 greenz red1 yellow2 redi red2 greeni redz yellow1 red2 pH Neutralization A pH neutralization system mixes a substance of unknown acidity with a neutralizer until the desired pH level is achieved e g in wastewater treatment An example process adapted from 17 operates as follows gt Traffic signal attacks can cause significant congestion 20 From Source tl al oe Neutralizer vi v2 heater Is3 ts Is5 as _ t i 4 Ls NXE mixer start v4 U3 To Source To Next Step When the tank level is below ls3 valve v1 is opened to fill the tank with the acidic substance up to level Js3 At this point valve v2 is opened to dispense the neutralizer until the correct acidity level is indicated by the acidity sensor as T and the correct temper ature of the product has been reached as indicated by temperature sensor ts T If ts L the heater is activated If the desired pH level is not achieved before the tank fills to 1s3 v2 is closed and va is opened to drain the tank back to level s3 Once the correct pH level and temperature are achieved and there is at least ls3 liquid in the tank it is
5. 37 proposed the use of a safety PLC to monitor plant behavior and detect deviations from deter ministic behavior Similarly a model based anomaly detection sys tem for SCADA networks was proposed in 10 Lemay et al 31 used attestation protocols to verify the integrity the code running on a smart electricity meter including firmware updates Attestations have also been used to prevent peripheral firmware from attacking a host computer 32 A similar method could be applied to con trol systems in which PLCs must attest their entire stack including firmware and control logic to a trusted third party before being al lowed to send control signals to devices Thus any maliciously uploaded control logic would be discovered Of course any such solution faces a long path to deployment in real world systems Control logic obfuscation If the above two measures fail obfus cation of the PLC s control logic can offer a final line of defense in preventing SABOT s analysis This has the added advantage that no modification of the control system is required beyond obfuscating the control logic itself Much of the existing work on program ob fuscation is has attempted either to evade malware signature match ing 48 or to prevent code injection into address spaces 47 Here the objectives are different the goal in this case is to prevent either decompilation or VTDM recovery by SABOT Attempts at pre venting decompilation will likely fail
6. L and updated according to the expression a Timer variables require an extra bit of state Recall that a PLC timer t T only when its input expression a T continuously for at least t s preset time duration Furthermore any input variable in the model may change state while the timer is expiring Thus for each timer must hold for two state transitions The first transi tion simulates the starting of the timer s countdown and the second simulates the expiration allowing the timer to output T An additional step is required for the preprocessing of bytecode Originally some Siemens bytecode contains the and before or instruction signified by the mnemonic O The O instruction breaks up a conjunction into a disjunction of conjunctions For example consider the following program x1 x2 x3 x4 y1 IPPOPP This is equivalent to y1 lt x1 A x2 V x3 A x4 This can be rewritten as O A xl A x2 O A x3 A x4 yl 3 3 VTDM Recovery Constraint NuSMV Model M VAR x boolean input x ASSIGN init x L next xz T L VAR y boolean output or local y ASSIGN c yea init y L next y a VAR t boolean tp boolean ASSIGN timer t init t 1 c tia next t aA tpVt T L init t L next tp a Table 2 Constructing M from constraints C Recall that the process specification is the adversary supplied de scription and expected beh
7. Networking and Security Research Center Technical Report NAS TR 0162 2012 SABOT Specification based Payload Generation for Programmable Logic Controllers Stephen McLaughlin and Patrick McDaniel 21 July 2012 The Pennsylvania State University 344 IST Building University Park PA 16802 USA http nsrc cse psu edu 2012 by the authors All rights reserved SABOT Specification based Payload Generation for Programmable Logic Controllers Stephen McLaughlin Systems and Internet Infrastructure Laboratory Pennsylvania State Univesity smclaugh cse psu edu ABSTRACT Programmable Logic Controllers PLCs drive the behavior of in dustrial control systems according to uploaded programs It is now known that PLCs are vulnerable to the uploading of malicious code that can have severe physical consequences What is not under stood is whether an adversary with no knowledge of the PLC s interface to the control system can execute a damaging targeted or stealthy attack against a control system using the PLC In this paper we present SABOT a tool that automatically maps the con trol instructions in a PLC to an adversary provided specification of the target control system s behavior This mapping recovers suffi cient semantics of the PLC s internal layout to instantiate arbitrary malicious controller code This lowers the prerequisite knowledge needed to tailor an attack to a control system SABOT uses an in cremental mod
8. V model checker of each experiment con ducted in Section 4 1 Note that SABOT s running time for a given model and specification is hard to calculate for a given set of in puts because it is highly dependent on the number of incremental mappings attempted Shown in Table 5 over 75 of tests the mapping is found in less than 10 seconds and in 90 of tests the mapping is found in less than 30 seconds Two tests however deserve particular atten tion The test with a running time of 1m43 6s for parallel traffic signaling made the most calls to the model checker of any test It also represented the greatest increase in calls to the model checker over its own baseline This can be attributed to the fact that the traf fic signal was the only specification containing specifications that Control Logic Baseline Emergency n n n fn nfn Annunciator Sequential Parallel Pad Y Os S 2 y dD L X g v ny eS O LCAN Control Logic YS Baseline Emergency n n n nf nj nj n n nf nj nin Annunciator p Sequential plpl l e p Parallel pl el el p p p p p Table 4 Per device accuracy results Empty cell Correct mapping p false positive mapping n false negative no mapping Shaded cell experiment omitted see description System Baseline Emergency Annunciator S
9. acks such as Stuxnet 18 a precompiled payload is not necessary An attack using SABOT proceeds as follows 1 The adversary encodes his understanding of the plant s be havior into a specification The specification contains a dec laration of plant devices and a list of temporal logic proper ties defining their behavior 2 SABOT downloads the existing control logic bytecode from the victim PLC and decompiles it into a logical model SABOT then uses model checking to find a mapping between the specified devices and variables within the control logic 3 SABOT uses the mapping to instantiate a generic malicious payload into one that can be run on the victim PLC The generic payload can contain arbitrary manipulation of the specified devices which SABOT substitutes with PLC ad dresses SABOT is not for adversaries that do not understand the behavior of the victim plant In such cases an adversary can erase the PLCs memory upload random instructions or attempt to bypass safety properties of the control logic 35 None of these attacks however are guaranteed to be effective or stealthy Instead SABOT is most useful to adversaries with accurate knowledge of the target plant and process but that are unaware of a critical piece of information how to manipulate specific plant devices from the PLC This infor mation is not obvious to the adversary because it is unknown which PLC variables are mapped to plant devices There are s
10. adversary intended Consider an example false positive mapping ur p start gt x2 Ua gt yo Judging by the same criteria as above we can see that 1 urp sbutton holds under the control logic but criterion 2 fails because x2 and y2 the mid level switch and the B in gredient valve respectively are not the names of control variables intended by the adversary This raises the question how can the adversary remove this ambiguity from the specification without a priori knowledge of the semantics of x1 2 y1 and y2 While the adversary does not know the semantics of names in Vm he does know the semantics of names in Vy Thus the adver sary need not know that x2 is a name for a mid level switch and not a start button only that there is some control variable name that corresponds to a mid level switch But the adversary already has an abstraction for this the name l3 The same goes for y2 and its abstraction the name vg Thus the adversary can reliably remove this ambiguity by checking which names in Vy are in conflict with names in the property sbutton For example consider a specifica tion that has the same structure as sbutton but with different names Read Switch 2 activates valve B cflict input 15 output vg INIT l3 15 gt AX ug Because the correct mapping for cflict differs from the correct mapping for sbutton we have that l3 conflicts with start and Ug conflicts with va If the adversary can remove th
11. alve Intuitively this control system never dispenses A but rather fills the tank with B Unfortunately the adversary does not know how to specify to the PLC which device is meant by Valve A or Start Button This is because PLCs do not necessarily label their I O devices with semantically meaningful names like Drain Valve Instead PLCs use memory addresses e g 1 Y2 to read values from and write values to sensors and physical devices We refer to this set of address names as Vm The adversary who does not know the semantics of the names in Vm prefers to use the set of semantically meaningful names Vz Start Button Valve B This raises the problem How can an adversary project attack Some PLCs such as the Rockwell Controllogix line allow pro grammers to give names to I O ports but these names are still of no use autonomous malware Desc Bytecode Accumulatora Stack And z A a z Nested Or O T x V And z2 A 2x2 T2 gi eV And y A y 2 Y TSV Pop stack z V a2 A y1 Store a to y2 y2 a Ce CU y2 amp x1 V x2 A y1 Vm Vm U z1 2 Y1 yo Table 1 Example accumulation of a constraint payloads using names in Vy onto a system that uses the unknown memory references Vm One of SABOT s main tasks is to find a mapping from the names in Vz to those in Vm Here SABOT re quires one additional piece of information from the adversary a specification of the targ
12. ariables in multiple subsystems share a dependency While this was not an issue in our experiments we defer a more sophisti cated dependency analysis algorithm to future work The performance and accuracy results are shown in Table 6 Only a single false positive mapping occurred from the specifica tion for motor control onto the implementation of railway switch ing Unlike the performance results in Section 4 3 here the railway switching has the highest running time This is due to the large number of incremental false positive mappings that occur when testing the railway switching specification against pH neutraliza tion which led to many false positive variable mappings being re jected by the incremental mapping algorithm Nevertheless in all cases the run times are still within the limits found in Section 4 3 Emergency Annunciator p Sequential plpl l ep p Parallel Table 7 Accuracy improvements on results from Table 4 Specified Run time s Calls FP Container Filling 3 28 96 0 Motor Control 4 70 138 1 Traffic Signal 18 28 485 0 pH Neutralization 6 49 174 0 Railway Switching 75 70 2057 0 Table 6 Run time s total checker calls and false posi tives for checking each specification against the monolithic con trol logic The motor control specification was incorrectly matched against the railway switching subsystem 4 5 Accuracy Imp
13. as control engineers expect to be able to read code from a PLC and decompile it Most PLC development environments can decompile control logic A more promising route is to add noise in the form of unused variables that are not mapped to any devices This would however be a funda mental departure from current control engineering practices 6 RELATED WORK SABOT sits at the intersection between the automated verifica tion of control systems and automated exploitation tools We now consider the conceptual contributions of both to SABOT Much work has been done to automatically verify safety properties in rail 19 26 chemical 38 and manufacturing 5 control sys tems Methods used for verification include model checking 52 and bounded model checking 21 linear system solving 42 and Petri Nets 22 No method has been proposed that allows for veri fication without knowledge of the VTDM Exploit frameworks like Metasploit 34 use collections of known exploits to partially automate the task of vulnerability testing These frameworks have been extended to attacks against SCADA and control systems 29 While exploitation of control systems is how ever not new 7 the rate of release of new SCADA and PLC ex ploits has been accelerating 44 12 McLaughlin described the requirements for extending exploitation frameworks to perform at tacks against PLCs in 35 SABOT is to the best of our knowledge the first implemetation an
14. aviors of some plant devices SABOT at tempts to find a Variable To Device Mapping VTDM p from names in the specification to names in the control logic model M If the correct mapping is found then the semantics are known for each name in Vm mapped to by p A specification is an ordered list of specifications A specifica tion with name id has the following syntax id lt input input list gt lt output output list gt lt INIT init input list gt lt UNIQUE gt As an example we can now restate our earlier specification for the plant start button When the start button is pressed the valve for ingredient A opens as the following specification sbutton sbutton input start output va INIT start start gt AX va The only mandatory part of a specification is the property which is defined in Computational Tree Logic CTL 23 Interpreta tions are given in quotes for the unfamiliar reader The CTL spec ification is defined over names given after the input and output keywords where input list U output list C Vy The SABOT checker will check this under the control logic model M in three steps 1 Choose wu input list U output list gt 9 Vm 2 Apply u to by substituting all names in with their map pings in u This is denoted by y read The property under the mapping ju 3 Check M H pu These three steps are applied over all possible mappings for a given specification There a
15. d demonstration of these techniques 7 CONCLUSION In this paper we have presented SABOT as a means to lower the bar of sophistication needed to construct payloads for vulner able PLCs If an adversary is familiar enough with their target to specify a precise attack definition then SABOT can map a supplied behavioral specification onto the code from the victim PLC allow ing a malicious payload to be instantiated We have demonstrated that even when unexpected features or independent subsystems are implemented in a PLC SABOT can still find a sufficient mapping to instantiate a payload for the system within a reasonable time frame PLC code obfuscation may prove an effective defense against such attacks though it is in conflict with current practices 8 1 2 REFERENCES Shodan http www shodanhq net ADVANTECH BROADWIN WEBACCESS RPC VULNERABILITY ICS CERT Advisory 11 094 02 April 2011 SIEMENS SIMATIC HMI AUTHENTICATION VULNERABILITIES ICS CERT Advisory 11 356 01 December 2011 Saurabh Amin Xavier Litrico S Shankar Sastry and Alexandre M Bayen Stealthy Deception Attacks on Water SCADA Systems In Proceedings of the 13th ACM international conference on Hybrid systems computation and control 2010 J M Roussel B Zoubek and M Kwiatkowska Towards Automatic Verification of Ladder Logic Programs In Proc IMACS Multiconference on Computational Engineering in Systems Applications CESA 2003 Dillon Beresfo
16. drained to the next stage by v3 The temperature and acidity lights tl and al are activated when the desired temperature and acidity have been reached respectively and the tank is at least at level ls3 Railway Switching Lastly consider a process that safely coordi nates track switches and signal lights on a real railway segment 19 b a EO H gt a try b s s ae amp fe d tra st HO GA 5 c The segment consists of the two tracks tr and tr2 two switches s and s2 and four signal lights a d A switch is said to be in the normal state if it does not allow a train to switch tracks and in the reverse state if it does allow a train to switch tracks If a signal is ON it indicates that the train may proceed and if it is OFF the train must stop The direction of each signal is indicated by an arrow The signalman can control the state of the lights and switches using the inputs sj s5 and a d where sj T puts switch s into reverse and a turns signal a ON To ensure safe operation the control logic maintains several invariants over the signal and switching commands from the signalman 1 Two signals on the same track e g a and b can never be ON simultaneously 2 If a switch is in reverse then at most one signal is allowed to be ON 3 a If switch s is in reverse then signals a and c must be OFF 3 b If switch s2 is in reverse then signals b and d must be OFF 4 If both sw
17. e con trol offered to an adversary by PLCs and the vulnerability of PLCs relative to the other two For example hundreds of Internet ad dressable PLCs can be found on the Shodan computer search en gine 1 14 and new web enabled PLCs are being released into the market place with the aims of making remote management more convenient 49 13 An even more common arrangement is to have the control system network connected to a corporate network for economic reasons 53 43 Given this requirement it is indeed the case that all but the most critical PLCs will be at least reachable from public networks In this work we consider an adversary that has sufficient knowl edge about the behavior of the target control system to design a tar geted and perhaps stealthy payload for that control system While this may sound like a strong requirement it is important to note that there are several methods through which one can obtain such information Many control systems including railway switching and electrical substations exhibit some or all of their machinery and behavior in plain view Furthermore details about plant struc ture can be gleaned from vulnerable human machine interfaces 3 2 and scanning of industrial network protocols 35 Vendors also release device data sheets and sample control logic precisely defin ing device behavior for example 27 Of course such information is available to low ranking insiders 30 Finally we menti
18. e specification is written as one or more temporal logic for mulas Var C Ve with some additional hints for SABOT For a given mapping p the adversary supplied payload or spec ification under p denoted u payload or j4 is identical to the original except with any names from Vz replaced by names from Vm Thus to check whether a given mapping u maps Vz to the devices is correct SABOT checks M E u Read The temporal logic formula with literal names mapped by ut holds over the labeled transition system M If these checks are satisfied under a given p then SABOTinstantiates the payload over Vz into a payload over Vm 3 2 Decompilation To obtain a process model M SABOT must first bridge the gap between the bytecode level control logic and the model itself This means decompiling a list of assembly mnemonics that execute on an accumulator based architecture into a labeled transition system defined over state variables SABOT performs this decompilation in two steps 1 The disassembled control logic bytecode is con verted to an intermediate set of constraints C on local output and timer variables from the PLC 2 The constraints in C are then translated to M using the modeling language of the NuSMV model checker 11 For step 1 the constraints are obtained via symbolic execution of the bytecode This requires a preprocessing to remove nonstandard instructions not handled by our symbolic execution The result
19. el checking algorithm to map a few plant devices at a time until a mapping is found for all adversary specified devices At this point a malicious payload can be compiled and uploaded to the PLC Our evaluation shows that SABOT correctly compiles payloads for all tested control systems when the adversary cor rectly specifies full system behavior and for 4 out of 5 systems in most cases where there where unspecified features Furthermore SABOT completed all analyses in under 2 minutes 1 INTRODUCTION Process control systems are vulnerable to software based exploits with physical consequences 18 41 33 44 43 55 46 4 28 40 The increased network connectivity and standardization of Super visory Control and Data Acquisition SCADA have raised con cerns of attacks on control system managed infrastructure 7 24 8 53 Modern control systems use Programmable Logic Controllers PLCs to drive physical machinery according to software control logic For ease of modification control logic is uploaded to the PLC from the local network the Internet or serial port 49 13 For example hundreds of Internet accessible PLCs and SCADA devices can be found through the Shodan search engine 1 14 An adversary with PLC access can upload malicious control logic called the payload thereby gaining full control of the devices under the PLC Nevertheless an additional challenge still remains Even with knowledge of the target control system s
20. entations of a traffic light control logic and results evaluated in Section 4 2 e Performance is the ability to efficiently recover the VTDM for a given specification We evaluate not only the total run ning time but the number of false positives encountered by the incremental mapping process in Section 4 3 e Scalability is the ability to perform accurately and efficiently as additional control system functionality is added to the PLC We augment SABOT with a basic dependency graph analysis and evaluate both accuracy and performance for PLCs run ning multiple independent subsystems Section 4 4 Note that this is the first set of experiments on SABOT and addi tional future studies providing further validation and enlightenment are appropriate However the results of this initial study indicate that SABOT works well on a variety of control logics and that there remain numerous avenues for engineering and fine tuning results We evaluate the use of two such improvements to refine our initial results in section 4 5 All experiments are conducted using the five variants of five rep resentative process control systems taken from real world applica tions described in Table 3 Each process description is used to im plement a specification and a control logic All specifications were created independently of the implementations Note that control variables are denoted using emphasis and input variable are anno tated with e g in
21. equential Parallel Container Filling 0 59 16 0 68 21 1 03 28 1 00 27 1 57 29 Motor Control 0 23 7 0 26 7 0 45 14 0 86 19 Traffic Signal 5 59 125 6 35 130 51 76 1040 103 60 1385 pH Neutralization 2 42 70 3 67 101 4 55 100 14 16 228 11 51 179 Railway Switching 0 92 25 1 05 27 4 00 97 19 95 97 Table 5 Running time s number of calls to the model checker for each system and case mapped three names at once Also note the comparative running times and number of checker calls for the sequential and parallel railway switching tests Both required the same number of calls to the checker but the parallel case has nearly a fivefold increase in running time The extended running time for each call to the checker was the result of the dif ference in state space between the two In the sequential case there were two systems with one set of inputs and the second system dependent on the first In the parallel case the independent input sets greatly inflated the model s state space We discuss a check that could reduce state space explosion in the following section 4 4 Scalability Thus far we have assumed that the control logic only contained the specified functionality In this section we evaluate SABOT s accuracy and performance given a PLC that has functionality for additional independent subsystems in place In practice a large fa cility such as a nuclear power plant or waste water treatment facil ity will be bro
22. erence on Computer and Communications Security November 2009 David Mayor K K Mookhey Jacopo Cervini and Fairuzan Roslan Metasploit Tookit for Penetration Testing Exploit Devevlopment and Vulnerability Research Syngress 2007 Stephen McLaughlin On Dynamic Malware Payloads Aimed at Programmable Logic Controllers In 6th USENIX Workshop on Hot Topics in Security 2011 Yilin Mo and Bruno Sinopoli False data injection attacks in control systems In Proceedings of the First Workshop on Secure Control Systems SCS 2010 Sibin Mohan Stanley Bak Emiliano Betti Heechul Yun Lui Sha and Marco Caccamo S3A Secure System Simplex Architecture for Enhanced Security of Cyber Physical Systems http arxiv org 2012 Il Moon Gary J Powers Jerry R Burch and Edmund M Clarke Automatic Verification of Sequential Control Systems Using Temporal Logic AIChE Journal 38 67 75 1992 National Energy Regulatory Comission NERC CIP 002 1 Critical Cyber Asset Identification 2006 Teague Newman Tiffany Rad and John Strauchs SCADA amp PLC Vulnerabilities in Correctional Facilities White Paper 2011 David M Nicol Hacking the Lights Out Scientific American 305 1 70 75 July 2011 T Park and P I Barton Formal Verification of Sequence Controllers Computers amp Chemical Engineering 2000 Ludovic Pi tre Cambac d s Marc Trischler and G ran N Ericsson Cybersecurity Myths on Power Control Systems 21 Misconcepti
23. et behavior If the adversary is to write a payload such as the one above for the mixing plant then it is assumed that he knows some facts about the plant For example the adversary can make statements like The plant contains two ingredient valves and one drain valve and When the start button is pressed the valve for ingredient A opens The adversary encodes such statements into a behavioral specification of the target plant When SABOT is then given a spec ification and control logic from a plant PLC it will try to locate the device addresses that behave the same under the rules of the logic as the semantically meaningful names in the adversary s specifica tion Like the payload the sensors and devices specified in the spec ification are defined using semantically meaningful names from Vy Given a control logic implementation SABOT will construct a model M from the control logic Var M Vm and perform a model checking analysis to find the Variable To Device Mapping VTDM u Vy Vm SABOT assumes it has the correct mapping u when all properties in the specification hold under the control logic after their names have been mapped according to u For example the above property When the start button is pressed the valve for ingredient A opens will be checked as Under the rules of the control logic When lt 4 is pressed then y opens un der the mapping u Start Button gt x4 Valve A gt yi Th
24. et control logic out of a number of candidates in Section 4 4 3 Room for error Using a precompiled payload an adversary s understanding of the plant s behavior must be exactly correct or the payload will likely fail Using a dynamically generated pay load there is some room for error For example in Section 4 5 we describe a method for writing behavioral specifications that will correctly map to a control logic regardless of whether or not it im plements an emergency stop button a common feature in many control systems While this is a first step towards making a truly adaptable attack mechanism our results show that it works well when an adversary correctly specifies the behavior of a majority of plant devices as shown in Section 4 1 It is also to the best of our knowledge the first analysis of its kind directed at PLC based control systems Our evaluations of SABOT show that it performs accurately and efficiently against control logics of equal or greater complexity than the target of the Stuxnet attack 18 We begin our discussion of SABOT in the next section by providing a brief overview of se quential control systems and detail an illustrative example 2 CONTROL SYSTEMS Control systems are used to monitor and control physical pro cesses These systems can drive processes as simple as motion ac tivated light switches or as complex as wastewater treatment Re gardless of their purpose and complexity control systems are
25. everal implications stemming from the existence of a tool like SABOT 1 Reduced adversary requirements In most cases the only way to know which PLC memory addresses map to which devices is to physically inspect the labels on wires connecting the PLC to de vices Only the most powerful adversaries e g insiders or nation Sabots were wooden shoes thrown into the gears of machinery by Luddites in the Industrial Revolution states will have this information 54 Furthermore SABOT en ables attacks by adversaries that are unfamiliar with PLC instruc tion set architectures and communication protocols Because the variable mapping is done on an intermediate representation code from arbitrary PLCs can be decompiled for analysis by SABOT We give an example implementation of one such decompiler in Sec tion 3 2 2 Improved target identification In the Stuxnet attack PLC ver sion strings and device metadata were used to verify that the correct target had been identified 18 If this metadata was not found in the PLC then it was silently ignored by the virus Using SABOT a target is identified by whether or not its control logic behaves in the way specified by the adversary Thus the adversary need not know any version strings or vendor metadata a priori This may also re duce false positives in cases where an unintended PLC contains the expected version strings and metadata We evaluate SABOT s abil ity to correctly identify a targ
26. gen erally structured the same The physical apparatus in which the control system resides is called the plant Within the plant control systems can be decom posed into three distinct elements control inputs control outputs and control logic Control inputs are used to communicate the state of the plant For example temperature motion or light sensors are used to detect and communicate physical states Other inputs are human driven such as switches dials and buttons The control system sends output signals to external devices to effect changes in the physical world For example such signals may turn on indi cator lights open and close valves or drive bi directional motors The control logic is the PLC software that computes new outputs based on sensor inputs The PLC repeatedly executes the control logic in a scan cycle consisting of i read new inputs ii execute control logic and iii write outputs to devices An example control system for a simplified chemical mixer is shown in Figure 1 The plant Figure 1 a is a single mixer with valves to dispense two ingredients A and B a mixing element and a valve for draining the tank The valves are controlled by the output variables yi and y2 respectively the mixer by y3 and the drain by ya A device is ON when its corresponding output variable is set to T true and OFF when it is false Three level sensors are used to detect when the tank is at three levels low half ful
27. ing code conforms to the IEC 61131 3 standard for PLC instruction lists 25 The control flow graph CFG of the resulting code is constructed and a symbolic execution is done over the CFG accord ing to a topological ordering Several register values are tracked most importantly the logic accumulator a An example symbolic accumulation of control logic is shown in Table 1 Step 2 translates the set of constraints resulting from step 1 into a control logic model M that can be evaluated by the NuSMV model checker NuSMV takes definitions of labeled transitions systems with states consisting of state variables SABOT uses the VAR boolean expression to declare a state variable for each name in Vm Each Boolean variable is first initialized using the init expression and updated at each state transition using the next expression A Boolean variable may be initialized or updated to a constant value of T or L another expression or a nondeterministic assignment 7 1 where both transitions are considered when checking a property For a complete specification of the NuSMV input language see 9 As shown in Table 2 there are three translation rules In the case of input variables a new Boolean variable is declared initialized to L and updated nondeterministically The nondeterministic update is necessary because all possible combinations of sensor readings must be factored into the model Output and local variables are initialized to
28. is conflict then the false positive mapping urp will also be removed and the am biguity is resolved The conflict can be removed by the addition of the following specification Read Valve A can be on with the start button released sbindep input start output va EF start A va To see that the pair sbutton sbindep removes the conflict we can substitute the conflict into sbindp giving EF l gt A vs which does not hold under the control logic Thus if the con flicting mapping is initially made when checking sbutton this mapping will fail when checking sbindep which will cause the SABOT checker to go back to sbutton and search for another mapping in this case the correct one Of course this approach is not guaranteed to make a completely unambiguous specification as will be seen in Section 4 but it does remove all ambiguities with respect to devices the adversary is aware of In larger examples we keep track of conflicts and resolutions us ing conflict tables An example set of conflict tables for a specifica tion of a chemical process is shown in Figure 3 Each specification has a potentially empty conflict table listing all unmapped names in V that satisfy the specification Given a nonempty conflict table for a specification spec one can make spec unambiguous by writ ing at most one additional specification over the names in spec for each entry in its conflict table This guarantees a finite specifica
29. itches are set to reverse then all signals must be OFF Each of the applications is implemented in a Baseline control sys tem Each baseline system is then modified with four variants to introduce plant features not anticipated by the baseline specifica tions Emergency This case adds an emergency shutdown button named estop to each plant If the emergency shutdown button is pushed all devices will be immediately turned OFF One can see how this can cause false negative mappings For example a property of the form AG input AX output will no longer hold because of the case where input estop holds but output is forced to L The motor controller s stop button acts as a shutdown so there was no need to add one Annunciator Annunciator panels are visual or sometimes audible displays present within the plant itself For safety reasons they are wired directly to the PLC and used to indicate if there is a condi tion in the plant that should require special precautions by humans on the plant floor We place a single annunciator light on each in put and output in the plant This light is turned ON by the control logic if the corresponding input or output is ON and OFF other wise We evaluate the plants with annunciator panels because the annunciator variables nearly double the number of control variables that are expected by the adversary The traffic signal and railway switching processes were not evaluated with annunciator panel
30. ken down into subsystems each of which will have a dedicated PLC These PLCs are in turn coordinated by higher levels of supervisory control However this does not guarantee that ad ditional unspecified functionality will not be run on the same PLC Thus we wish to evaluate SABOT under such a scenario In this section we augment SABOT with a simple dependency analysis that separates the control logic into separate models for each independent subsystem The subsystem models are constructed as follows First the variable dependency graph for the control logic is constructed Second an undirected edge is added between any two output variables with a common dependency Third a new graph is constructed using just the output variables and newly added undirected edges A single subsystem model is constructed for each strongly connected component in this graph The specifi cation is then tested against each model independently To simulate independent subsystems running in the same PLC we combined all five test systems into a single monolithic control logic We then ran SABOT with the dependency analysis against the monolithic logic with each of the five specifications Ideally in each run SABOT would match the specification only to the correct corresponding subsystem There are two types of errors that can occur here First a specification could be mapped to an incorrect subsystem Second an incorrect dependency analysis may occur e g if v
31. l and full corresponding to inputs 71 x2 and x3 respectively A level switch x T if the contents of the tank are at or above its level A start signal is sent to the PLC via x4 The mixer follows a simple process in which ingredient A is added until the tank is half full ingredient B is mixed with A until the tank is full and the result is drained The specification shown in Figure 1 b details the control system implementation 1 Initially all inputs and outputs are off until the Start button is pressed x4 T 2 At this point the process enters state Fill A yi T and the tank is filled with ingredient A until the tank is filled midway x2 T at which point the valve for A is closed y L 3 Next the system transitions to the state Mix B in which in gredient B is added valve B is opened until cs T The mixer y3 is also started in this state 4 At this point the system closes the value for B and enters the Drain state ys T until the tank is empty detected by the low sensor x L At this point the mixer is stopped The mixing process is an example of a common class of control sys tems called sequential control systems Sequential control systems drive a physical plant through a process consisting of a sequence of discrete steps Sequential control is used in industrial manu facturing automotive assembly QA testing building automation elevators lighting chemical processing proce
32. lantwide Process Control Wiley Inter Science 1999 Robert P Evans Control Systems Cyber Security Standards Support Activities January 2009 15 16 17 Albert Falcione and Bruce Krogh Design Recovery for Relay Ladder Logic In First IEEE Conference on Control Applications 1992 18 Nicholas Falliere Liam O Murchu and Eric Chien W32 Stuxnet Dossier http www symantec com 2010 19 Nelson Guimaraes Ferreira and Paulo S rgio Muniz Silva Automatic Verification of Safety Rules for a Subway Control Software In Proceedings of the Brazilian Symposium on Formal Methods SBMF 2004 Shelby Grad Engineers who hacked into L A traffic signal computer jamming streets sentenced http latimesblogs latimes com J F Groote S E M van Vlijmen and J W C Koorn The Safety Guaranteeing System at Station Hoorn Kersenboogerd In Computer Assurance 1995 Proceedings of the Tenth Annual Conference on Systems Integrity Software Safety and Process Security pages 57 68 June 1995 M Heiner and T Menzel Instruction List Verification Using a Petri Net Semantics In JEEE International Conference on Systems Man and Cybernetics volume 1 pages 716 721 1998 Michael Huth and Mark Ryan Logic in Computer Science Cambridge University Press 2004 Vinay M Igure Sean A Laughter and Ronald D Williams Security Issues in SCADA Networks Computers and Security 2006 International Electrotechnical Commission Internatio
33. nal Standard IEC 61131 Part 3 Programming Languages Phillip James and Markus Roggenbach SAT based Model Checking of Train Control Systems In Proceedings of the CALCO Young Researchers Workshop 2009 KEYENCE America Position control using a stepper motor http www keyence com downloads plc_dwn php 20 21 22 23 24 25 26 27 28 Brian Krebs Cyber Incident Blamed for Nuclear Power Plant Shutdown http www washingtonpost com June 2008 Joel Langill White Phosphorus Exploit Pack Ver 1 11 Released for Immunity Canvas http scadahacker blogspot com 2011 30 Nicholas Leall Lessons from an Insider Attack on SCADA 29 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 Systems http blogs cisco com security lessons_from_ an_insider_attack_on_scada_systems August 2009 Michael LeMay and Carl A Gunter Cumulative attestation kernels for embedded systems In Proceedings of the 14th European Symposium on Research in Computer Security ESORICS 2009 Yanlin Li Jonathan M McCune and Adrian Perrig Viper verifying the integrity of peripherals firmware In Proceedings of the 18th ACM conference on Computer and communications security Yao Liu Peng Ning and Michael K Reiter False Data Injection Attacks against State Estimation in Electric Power Grids In Proceedings of the 16th ACM Conf
34. ndependent processes 4 1 Accuracy Recall that accuracy is a measure of the correctness of the iden tified mappings between internal devices and the process specifica tions i e the accuracy of the VTDM Here we measure correctly mapped devices incorrect mappings false positives and failures to identify any mapping at all false negatives The results for ac curacy experiments are shown in Table 4 To summarize in three out of five test systems the baseline specification is sufficient to produce a complete correct mapping for the control system and four out of five systems had no false positives As expected the emergency shutdown case caused false nega tives in two out of the three control systems This was due to the failure of specifications of the form AG input output to always hold under any mapping when there is always a state in which estop makes the property not hold The false negatives occur for all devices in both cases because later specifications con tained names that failed to map in earlier specifications making them uncheckable The pH neutralization system experienced the most false pos itives due to its multiple parallel behaviors In the annunciator panel the behavior of the valve for the neutralizer v2 could not be distinguished from the annunciator light for the mid level switch ls3 because 1s3 T implies that both the valve and annunciator light are ON More broadly the sequential system false po
35. on that while it is unlikely that unskilled or script kiddie adversaries will mount attacks targeted at specific devices there is existing work describing such naive attacks and their limitations 35 3 SABOT SABOT instantiates malicious payloads for targeted control sys tems Depicted in Figure 2 the SABOT initially extracts a logi cal model of the process from the PLC code see Section 3 2 De compilation Next the model and process specification are used to create a mapping of physical devices to input and output vari ables called the variable to device mapping or VTDM see Sec tion 3 3 VTDM Recovery Last a generic attack is projected onto to the existing model and VTDM to create a malicious payload called the PLC Malcode see Section 3 4 Payload Construction This malcode is delivered to the victim interface Decompilation kK PLC Code Model Process Specification Generic Malcode Payload VTDM Recovery VTDM pl Payload Construction PLC Malcode Figure 2 SABOT Generating a malicious payload for a target control system based on process specification the PLC code and generic malcode 3 1 Problem Formulation Consider a scenario in which an adversary may wish to cause ingredient A to be omitted from the chemical mixing process de scribed above A PLC payload for this might look like Valve A L Valve B Start Button V Valve B A Drain V
36. ons and False Beliefs IEEE Transactions on Power Delivery 2011 Jonathan Pollet Electricity for free the dirty underbelly of scada and smart meters In Proceedings of Black Hat USA 2010 July 2010 Venkat Pothamsetty and Matthew Franz The SCADA Honeynet Project http scadahoneynet sourceforge net P F Roberts Zotob PnP Worms Slam 13 DaimlerChrysler Plants http www eweek com August 2008 Hovav Shacham Matthew Page Ben Pfaff Eu Jin Goh Nagendra Modadugu and Dan Boneh On the Effectiveness of Address Space Randomization In Proceedings of the 11th ACM conference on Computer and communications security CCS 2004 Peter Szor The Art of Computer Virus Research and Defense Addison Wesley 2005 12 49 Triangle Research International Connecting Super PLCs to the Internet http www tri plc com internetconnect htm 50 U S Department of Energy Office of Electricity Delivery and Energy Reliability A Summary of Control System Security Standards Activities in the Energy Sector October 2005 51 Joe Weiss Are the NERC CIPS making the grid less reliable Control Global 2009 Kirsten Winter Model Checking Railway Interlocking Systems In Proceedings of the Twenty fifth Australasian Conference on Computer Science ACSC 2002 Tim Yardley SCADA Issues Vulnerabilities and Future Directions ogin 34 6 14 20 December 2008 Kim Zetter Clues Suggest Stuxnet Virus Was Built for Subtle Nuclear Sabotage h
37. pplica tions are Container Filling Consider the filling of product containers on an assembly line e g cereal boxes 15 In the basic process a belt belt carries an empty container belt T until it is under the fill bin as indicated by a condition cond e g a light barrier detects when container is in position Thereafter a fill valve fill is opened for a period of time to fill and the belt is activated to move the next container into place It may also occur that the fill bin itself is depleted as indicated by a level sensor low and a secondary source bin with valve source will be used to replenished the fill bin Motor Control Stepper motors provide accurate positioning by dividing a full rotation into a large number of discrete angular po sitions This has many applications in precision machining equip ment like lathes and surface grinders and conveyor belts Most stepper motors also offer bidirectional operation A motor con troller for a stepper motor will allow for starting the motor in the forward direction fon reversing the motor ron such that fon V ron always holds Buttons are used for selecting forward for and reverse rev operation and stopping the motor stop Larger motors that require spin down times before changing direction are equipped with timers that do not allow for the motor to be started in its opposite direction until it has been stopped for several seconds Traffic Signaling Consider
38. rd Exploiting Siemens Simatic S7 PLCs In Black Hat USA 2011 Eric Byres and Justin Lowe The Myths and Facts behind Cyber Security Risks for Industrial Control Systems In ZSA Process Control Conference 2003 3 4 5 6 7 8 Alvaro A C rdenas Saurabh Amin and Shankar Sastry Research Challenges for the Security of Control Systems In Proceedings of the 3rd conference on Hot topics in security 2008 Roberto Cavada Alessandro Cimatti Charles Arthur Jochim Gavin Keighren Emanuele Olivetti Marco Pistore Marco Roveri and Andrei Tchaltsev NuSMV 2 5 User Manual 2010 Steve Cheung Bruno Dutertre Martin Fong Ulf Lindqvist Keith Skinner and Alfonso Valdes Using Model based 9 10 11 Intrusion Detection for SCADA Networks In Proceedings of the SCADA Security Scientific Symposium 2007 A Cimatti E Clarke F Giunchiglia and M Roveri NuSMV A New Symbolic Model Verifier In Computer Aided Verification Springer Berlin Heidelberg 1999 Lucian Constantin Researchers Expose Flaws in Popular Industrial Control Systems http www pcworld com January 2012 Control Technology Corp Blue Fusion Model 5200 Controller http www ctc control com products 5200 5200 asp 11 12 13 14 ireann P Levertt Quantitatively Assessing and Visualising Industrial System Attack Surfaces Master s thesis University of Cambridge 2011 Kelvin T Erickson and John L Hedrick P
39. re two more optional parts to each specification the list of inputs that will be initially ON INIT and the conflict resolution hint UNIQUE Any names in init input list will have their ini tial values set to T when checking M u while all other inputs will have initial value L This is useful for checking plant starting states The keyword UNIQUE declares that the names in input list and output list will not appear in any conflict mappings For a definition and discussion of conflict mappings see Section 3 3 2 3 3 1 Mapping Specifications to Models SABOT searches for a mapping Vs gt Vm such that M u1 for every specification in the specification This is done incrementally finding a satisfying mapping for each specification before moving to the next If no satisfying mapping is found for a given specification the previous specification s mapping is dis carded and it is searched again for another satisfying mapping If no more satisfying mappings are found for the first specification in the specification the algorithm terminates without identifying a mapping If a satisfying mapping is found for all specifications the algorithm accepts this as the correct mapping usar Algorithm 1 shows the basic mapping procedure except for the UNIQUE fea ture Algorithm 1 IncMapping Input u spec VM M Output The satisfying mapping usar or none if spec then USAT amp H return T foreach uo Var gt Vm do
40. rovements In this section we consider using two refinements to improve the accuracy results found in Section 4 1 First we include the dependency analysis introduced in the previous section in hopes of improving the results for the parallel variation in pH neutralization Second we introduce a method to safeguard a specification against the presence of emergency stop systems a common feature We safeguard a specification against an emergency stop button by slightly weakening each property of the form AG 4Y to al low it to fail on cases where y Aestop holds For example in the pH neutralizer the property AG gt mixer A Ist Als gt AX mizer was changed to AF mixer A Ist ls3 AX mixer anda fairness constraint FAIRNESS mixer was added to force the model checker to ignore the path on which estop was infinitely ON For properties of other forms such as AG 77 no such weak ening is necessary because it still holds when either 7 estop or w A nestop The results with both dependency analysis and safeguards are shown in Table 7 The safeguard was applied to all properties in the pH neutralization and traffic signal systems and all five test cases were rerun The addition of the safeguards did not negatively affect accuracy in the baseline case and the number of test cases for which all devices are mapped regardless of plant features is in creased to 4 out of 5 Thus if an adversary has reason to suspect that an emergenc
41. s as annunciator functionality is already present in both systems Sequential This case considers a plant with two distinct instances of the process where the second instance is dependent on the first For the motor controller this simply means that the second motor mimics the forward and reverse behavior of the second The same is true for the traffic lights where the state of the second mimics the first For sequential container filling containers are partially by the first system then by the second The railway switching exam ple is modified to include three tracks and allow a train to switch from the first track to a middle second track and then to the third track The safety properties are extended to prevent any conflicting routes between the three tracks Finally the chemical neutraliza tion process is serialized to two tanks such that the first process fully drains to the second before the second starts Parallel This case models two independent instances of the pro cess executing in parallel on the same PLC This is expected to occur in production environments where it is more cost effective to add more input and output wires to the same PLC than to maintain distinct PLCs for each parallel instance of the process A special criterion is added for the parallel case called Synchronized which is true if all mappings where true positives in the same instance of the process I e there is no mixing of mappings between the two i
42. sitives were caused by devices in the first instance that were mistaken for a device in the second instance For example the heater in the first instance of the pH neutralization system was confused with the heater in the second The false positives in the parallel case were caused by devices in the first instance that were mistaken for non equivalent devices in the second For example the finished product valve v3 in the first instance of the pH neutralization system was confused with the mixer in the second instance We improve upon these results in Section 4 5 4 2 Adaptability Adaptability is the ability to recognize a control system by its behavior independent of its implementation Because SABOT only considers control logic behavior and not its structure any imple mentation conforming to the process description will be handled equivalently To confirm this is the case and as an experimental control a team member not involved in prior analysis was tasked with implementing an alternative traffic signal control program that exhibited the behavior from the description The team member took an alternative strategy of allowing the light timers to drive the rest of the process resulting in a significantly different implementation The same experiments run above were rerun on this new implemen tation and the results were identical 4 3 Performance To gauge runtime costs we measured the running time and num ber of calls to the NuSM
43. ss control energy delivery power management and transportation automation rail way switching traffic lights among others Not shown in the example a timer is a special control system primitive that introduces a preset time delay between when an input becomes true and when a subsequent output becomes true A timer only sets the specified output to T when the input has been set to T for the duration of its preset delay value Timers can be used to replace other sensors For example the level sensors above could be replaced with timers presuming the flow and drain rates of the apparatus were known and fixed 2 1 PLC Logic and ISA The control logic for a sequential process is codified into a set of Boolean circuits that are evaluated in order with dependencies The circuits are then compiled into the PLC s native instruction set The control logic implementation of the chemical mixing pro cess is shown in Figure 1 c The PLC executes each of the four statements starting with Fill A and ending with Drain once each scan cycle At the plant start up state y1 L After the button x4 is pressed y T until x T Notice that the clause x4 V y1 is necessary as x4 is a button that may only be depressed temporarily thus once y is activated it should remain so until the terminating condition x2 T Here the value of y on the right hand side of the statement is the value for y from the previous scan cycle The control output
44. t the correct map ping can be recovered the majority of the time even when the plant has unexpected devices and functionality In the event that SABOT finds a correct VTDM but the adversary was unaware of some devices in the plant an instantiated payload Generic Payload Instantiated Payload uel ye L up start V vg A 713 y2 z4 V y2 A 723 ys x2 V ys A 1 y4 x3 V y4 Az mizer lt 13 V mixer A l Ug 13 Vv va A l System Container Filling Motor Control Traffic Signaling pH Neutralization Railway Switching Table 3 Control system variants omitted shaded can cause side effects that may reduce stealthiness or reduce the impact of the attack E g suppressing ingredient A in the chemical mixing process could result in a conspicuous failure later in the process The impact of side effects may be partially mitigated by the use of low profile attacks such as merely reducing the amount of ingredient A 4 EVALUATION This section details a validation study of SABOT focusing on four metrics e Accuracy is the ability of SABOT to correctly map a specifi cation onto a control system even when unexpected features are present We evaluate the number of devices that are cor rectly mapped in each test case in Section 4 1 e Adaptability is the ability to recognize different variants of a control system A canonical specification is tested against two unique implem
45. tion size bounded in O V specifications Significantly fewer are usually necessary in practice The specification keyword UNIQUE is used to declare that no name appearing in the specification will appear in a conflicting mapping This is useful because there are some cases where the same name appears in many conflict table entries See specifica tion sbutton in Figure 3 It is never required to use UNIQUE to remove conflicts but it can be useful in reducing the search space 3 4 Payload Construction In the payload construction step SABOT instantiates a generic malicious payload for the target PLC Given a VTDM vp for a vic tim PLC and specification SABOT uses u to map the names in the adversary s generic payload into those in the control logic There after the instantiated payload is recompiled into bytecode and up loaded to the PLC SABOT payloads are control logic programs defined over names in Vz Once the VTDM p is found the payload is instantiated under u producing a payload over names in Vm Using this ap proach an adversary can assume the same semantics for names in the payload that are assumed for names in the specification As an example the following payload manipulates the chemical mixing process into omitting ingredient A from the mixture Assuming that the correct mapping i e urp is found by SABOT then this payload will execute as expected when uploaded to the mixer PLC Our results in Section 4 1 show tha
46. ttp www wired com threatlevel 2010 11 stuxnet clues November 2010 Kim Zetter Attack code for scada vulnerabilities released online http www wired com threatlevel 2011 03 scada vulnerabilities 2011 52 53 54 55
47. var outvar below While seemingly sim ple most of the following systems have a larger variety of devices Ww x eer ae ae INIT start UNIQUE A valve INIT ls ls sa gt AX v AGC Is gt AX miser ls Als gt AX v 1 sbutton ia v2 L Ist v3 mpty 2 latched i RS 2 ls3 v4 tan 3 185 heater 3 ls tl valve 3 heateron 4 ls3 v4 z AG ls A ls3 A ls3 gt AX v4 gt 4 ls3 as 1 2 3 4 mixeron 5 Iss heater mpty 5 mizerindep 6 ts tl mixerindep re ne mizeron TARE aos T as al z 6 levelindep BE ie Asien he Anan AG as V ats A av3 gt AX 703 7 level latched re ne sbutton mpty mpty leve ae aloe EF start A AX start A v1 levelindep re ne mizeron tlight 3 a 9 valve4 EF ls A v1 AX Is A v1 AG ts gt AX tl i ae heateron UNIQUE mpty mpty ee AG ts AX heater level 11 tlight 15 ls v p light 12 pHlight 2 ist Do AG mizer A lst Als gt AX mizer AG as gt AX al 2 as v2 mpty mpty Figure 3 An unambiguous specification with conflict tables for the pH neutralization system and more complex state machines than the target of the Stuxnet attack many uniform variable speed drives 18 The five a
48. y stop system may be in place the use of safe guards can be an effective workaround 5 COUNTERMEASURES We now explore several avenues to countermeasures to SABOT like mechanisms in control systems improved perimeter security novel PLC security architectures and control logic obfuscation Improved perimeter security Perhaps the most straightforward way to safeguard against malicious PLC payloads is to improve perimeter defenses around PLCs Unfortunately the most effective solution disconnecting the PLC from any networked computer is neither common practice nor in many cases economically feasible 10 Due to economic constraints and for ease of maintenance PLCs are often connected to the corporate networks 53 or the Internet 49 13 However numerous standards exists for defense in depth secu rity in control systems across industries 16 such as in the power sector 50 39 Compliance with standards however can lead to a checklist approach to security that can ultimately give a false sense of security impact 51 43 A final defense in depth technique is the use of SCADA honeynets 45 outside of the protected perime ter to detect adversaries before they access production SCADA de vices Novel PLC security architectures PLCs as they exist today sup port virtually no security precautions short of basic passwords There are several basic architectural changes that can mitigate any PLC payload mechanism Mohan et al
Download Pdf Manuals
Related Search