Visible to the public Biblio

Found 5734 results

Filters: Keyword is Human Behavior  [Clear All Filters]
2017-05-17
Michalevsky, Yan, Nath, Suman, Liu, Jie.  2016.  MASHaBLE: Mobile Applications of Secret Handshakes over Bluetooth LE. Proceedings of the 22Nd Annual International Conference on Mobile Computing and Networking. :387–400.

We present new applications for cryptographic secret handshakes between mobile devices on top of Bluetooth Low-Energy (LE). Secret handshakes enable mutual authentication, with the property that the parties learn nothing about each other unless they have been both issued credentials by a group administrator. This property provides strong privacy guarantees that enable interesting applications. One of them is proximity-based discovery for private communities. We introduce MASHaBLE, a mobile application that enables participants to discover and interact with nearby users if and only if they belong to the same secret community. We use direct peer-to-peer communication over Bluetooth LE, rather than relying on a central server. We discuss the specifics of implementing secret handshakes over Bluetooth LE and present our prototype implementation.

Albazrqaoe, Wahhab, Huang, Jun, Xing, Guoliang.  2016.  Practical Bluetooth Traffic Sniffing: Systems and Privacy Implications. Proceedings of the 14th Annual International Conference on Mobile Systems, Applications, and Services. :333–345.

With the prevalence of personal Bluetooth devices, potential breach of user privacy has been an increasing concern. To date, sniffing Bluetooth traffic has been widely considered an extremely intricate task due to Bluetooth's indiscoverable mode, vendor-dependent adaptive hopping behavior, and the interference in the open 2.4 GHz band. In this paper, we present BlueEar -a practical Bluetooth traffic sniffer. BlueEar features a novel dual-radio architecture where two Bluetooth-compliant radios coordinate with each other on learning the hopping sequence of indiscoverable Bluetooth networks, predicting adaptive hopping behavior, and mitigating the impacts of RF interference. Experiment results show that BlueEar can maintain a packet capture rate higher than 90% consistently in real-world environments, where the target Bluetooth network exhibits diverse hopping behaviors in the presence of dynamic interference from coexisting Wi-Fi devices. In addition, we discuss the privacy implications of the BlueEar system, and present a practical countermeasure that effectively reduces the packet capture rate of the sniffer to 20%. The proposed countermeasure can be easily implemented on the Bluetooth master device while requiring no modification to slave devices like keyboards and headsets.

Snader, Robin, Kravets, Robin, Harris, III, Albert F..  2016.  CryptoCoP: Lightweight, Energy-efficient Encryption and Privacy for Wearable Devices. Proceedings of the 2016 Workshop on Wearable Systems and Applications. :7–12.

As people use and interact with more and more wearables and IoT-enabled devices, their private information is being exposed without any privacy protections. However, the limited capabilities of IoT devices makes implementing robust privacy protections challenging. In response, we present CryptoCoP, an energy-efficient, content agnostic privacy and encryption protocol for IoT devices. Eavesdroppers cannot snoop on data protected by CryptoCoP or track users via their IoT devices. We evaluate CryptoCoP and show that the performance and energy overheads are viable in a wide variety of situations, and can be modified to trade off forward secrecy and energy consumption against required key storage on the device.

Wang, Tianhao, Zhao, Yunlei.  2016.  Secure Dynamic SSE via Access Indistinguishable Storage. Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security. :535–546.

Cloud storage services such as Dropbox [1] and Google Drive [2] are becoming more and more popular. On the one hand, they provide users with mobility, scalability, and convenience. However, privacy issues arise when the storage becomes not fully controlled by users. Although modern encryption schemes are effective at protecting content of data, there are two drawbacks of the encryption-before-outsourcing approach: First, one kind of sensitive information, Access Pattern of the data is left unprotected. Moreover, encryption usually makes the data difficult to use. In this paper, we propose AIS (Access Indistinguishable Storage), the first client-side system that can partially conceal access pattern of the cloud storage in constant time. Besides data content, AIS can conceal information about the number of initial files, and length of each initial file. When it comes to the access phase after initiation, AIS can effectively conceal the behavior (read or write) and target file of the current access. Moreover, the existence and length of each file will remain confidential as long as there is no access after initiation. One application of AIS is SSE (Searchable Symmetric Encryption), which makes the encrypted data searchable. Based on AIS, we propose SBA (SSE Built on AIS). To the best of our knowledge, SBA is safer than any other SSE systems of the same complexity, and SBA is the first to conceal whether current keyword was queried before, the first to conceal whether current operation is an addition or deletion, and the first to support direct modification of files.

Fan, Shuqin, Wang, Wenbo, Cheng, Qingfeng.  2016.  Attacking OpenSSL Implementation of ECDSA with a Few Signatures. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :1505–1515.

In this work, we give a lattice attack on the ECDSA implementation in the latest version of OpenSSL, which implement the scalar multiplication by windowed Non-Adjacent Form method. We propose a totally different but more efficient method of extracting and utilizing information from the side-channel results, remarkably improving the previous attacks. First, we develop a new efficient method, which can extract almost all information from the side-channel results, obtaining 105.8 bits of information per signature on average for 256-bit ECDSA. Then in order to make the utmost of our extracted information, we translate the problem of recovering secret key to the Extended Hidden Number Problem, which can be solved by lattice reduction algorithms. Finally, we introduce the methods of elimination, merging, most significant digit recovering and enumeration to improve the attack. Our attack is mounted to the \series secp256k1\ curve, and the result shows that only 4 signatures would be enough to recover the secret key if the Flush+Reload attack is implemented perfectly without any error,which is much better than the best known result needing at least 13 signatures.

Picek, Stjepan.  2016.  Evolutionary Computation and Cryptology. Proceedings of the 2016 on Genetic and Evolutionary Computation Conference Companion. :883–909.

Evolutionary Computation (EC) has been used with great success on various real-world problems. One domain abundant with numerous difficult problems is cryptology. Cryptology can be divided into cryptography, that informally speaking considers methods how to ensure secrecy (but also authenticity, privacy, etc.), and cryptanalysis, that deals with methods how to break cryptographic systems. Although not always in an obvious way, EC can be applied to problems from both domains. This tutorial will first give a brief introduction to cryptology intended for general audience (therefore, omitting proofs and mathematics behind many concepts). Afterwards, we concentrate on several topics from cryptography that are successfully tackled up to now with EC and discuss why those topics are suitable to apply EC. However, care must be taken since there exists a number of problems that seem to be impossible to solve with EC and one needs to realize the limitations of the heuristics. We will discuss the choice of appropriate EC techniques (GA, GP, CGP, ES, multi-objective optimization, etc) for various problems and evaluate on the importance of that choice. Furthermore, we will discuss the gap between the cryptographic community and EC community and what does that mean for the results. By doing that, we will give a special emphasis on the perspective that cryptography presents a source of benchmark problems for the EC community. To conclude, we will present a number of topics we consider to be a strong research choice that can have a real-world impact. In that part, we give a special attention to cryptographic problems where cryptographic community successfully applied EC, but where those problems remained out of the focus of EC community. This tutorial will also present some live demos of EC in action when dealing with cryptographic problems. We will present several problems, ways of encoding solutions, impact of the algorithms choice and finally, we will run some experiments to show the results and discuss how to assess them from cryptographic perspective.

Wang, Timothy E., Garoche, Pierre-Loïc, Roux, Pierre, Jobredeaux, Romain, Féron, Éric.  2016.  Formal Analysis of Robustness at Model and Code Level. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. :125–134.

Robustness analyses play a major role in the synthesis and analysis of controllers. For control systems, robustness is a measure of the maximum tolerable model inaccuracies or perturbations that do not destabilize the system. Analyzing the robustness of a closed-loop system can be performed with multiple approaches: gain and phase margin computation for single-input single-output (SISO) linear systems, mu analysis, IQC computations, etc. However, none of these techniques consider the actual code in their analyses. The approach presented here relies on an invariant computation on the discrete system dynamics. Using semi-definite programming (SDP) solvers, a Lyapunov-based function is synthesized that captures the vector margins of the closed-loop linear system considered. This numerical invariant expressed over the state variables of the system is compatible with code analysis and enables its validation on the code artifact. This automatic analysis extends verification techniques focused on controller implementation, addressing validation of robustness at model and code level. It has been implemented in a tool analyzing discrete SISO systems and generating over-approximations of phase and gain margins. The analysis will be integrated in our toolchain for Simulink and Lustre models autocoding and formal analysis.

Maier, Petra R., Kleeberger, Veit, Mueller-Gritschneder, Daniel, Schlichtmann, Ulf.  2016.  Fault Injection at Host-compiled Level with Static Fault Set Reduction for SoC Firmware Robustness Testing. Proceedings of the Eleventh IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. :18:1–18:10.

Decreasing hardware reliability makes robust firmware imperative for safety-critical applications. Hence, ensuring correct handling of errors in peripherals is a key objective during firmware design. To adequately support robustness considerations of firmware designers during implementation, an efficient qualitative fault injection method is required. This paper presents a high-speed fault injection technique based on host-compiled firmware simulation that is suitable to analyze the impact of transient faults on firmware behavior. Additionally, fault set reduction by static code analysis avoids unnecessary injection of masked and equivalent faults. Application of the proposed fault injection technique on an industrial safety-relevant automotive system-on-chip (SoC) firmware demonstrates at least three orders of magnitude speedup compared to instruction set level. In addition, a fault set reduction by 78% is achieved. While significantly reducing the required fault injection time, the presented techniques provide as accurate feedback to the designer as existing state-of-the-art approaches.

Ng, Nicholas, Yoshida, Nobuko.  2016.  Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis. Proceedings of the 25th International Conference on Compiler Construction. :174–184.

Go is a programming language developed at Google, with channel-based concurrent features based on CSP. Go can detect global communication deadlocks at runtime when all threads of execution are blocked, but deadlocks in other paths of execution could be undetected. We present a new static analyser for concurrent Go code to find potential communication errors such as communication mismatch and deadlocks at compile time. Our tool extracts the communication operations as session types, which are then converted into Communicating Finite State Machines (CFSMs). Finally, we apply a recent theoretical result on choreography synthesis to generate a global graph representing the overall communication pattern of a concurrent program. If the synthesis is successful, then the program is free from communication errors. We have implemented the technique in a tool, and applied it to analyse common Go concurrency patterns and an open source application with over 700 lines of code.

Ostberg, Jan-Peter, Wagner, Stefan, Weilemann, Erica.  2016.  Does Personality Influence the Usage of Static Analysis Tools?: An Explorative Experiment Proceedings of the 9th International Workshop on Cooperative and Human Aspects of Software Engineering. :75–81.

There are many techniques to improve software quality. One is using automatic static analysis tools. We have observed, however, that despite the low-cost help they offer, these tools are underused and often discourage beginners. There is evidence that personality traits influence the perceived usability of a software. Thus, to support beginners better, we need to understand how the workflow of people with different prevalent personality traits using these tools varies. For this purpose, we observed users' solution strategies and correlated them with their prevalent personality traits in an exploratory study with student participants within a controlled experiment. We gathered data by screen capturing and chat protocols as well as a Big Five personality traits test. We found strong correlations between particular personality traits and different strategies of removing the findings of static code analysis as well as between personality and tool utilization. Based on that, we offer take-away improvement suggestions. Our results imply that developers should be aware of these solution strategies and use this information to build tools that are more appealing to people with different prevalent personality traits.

Nicolay, Jens, Spruyt, Valentijn, De Roover, Coen.  2016.  Static Detection of User-specified Security Vulnerabilities in Client-side JavaScript. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. :3–13.

Program defects tend to surface late in the development of programs, and they are hard to detect. Security vulnerabilities are particularly important defects to detect. They may cause sensitive information to be leaked or the system on which the program is executed to be compromised. Existing approaches that use static analysis to detect security vulnerabilities in source code are often limited to a predetermined set of encoded security vulnerabilities. Although these approaches support a decent number of vulnerabilities by default, they cannot be configured for detecting vulnerabilities that are specific to the application domain of the analyzed program. In this paper we present JS-QL, a framework for detecting user-specified security vulnerabilities in JavaScript applications statically. The framework makes use of an internal domain-specific query language hosted by JavaScript. JS-QL queries are based on regular path expressions, enabling users to express queries over a flow graph in a declarative way. The flow graph represents the run-time behavior of a program and is computed by a static analysis. We evaluate JS-QL by expressing 9 security vulnerabilities supported by existing work and comparing the resulting specifications. We conclude that the combination of static analysis and regular path expressions lends itself well to the detection of user-specified security vulnerabilities.

Su, Fang-Hsiang, Bell, Jonathan, Harvey, Kenneth, Sethumadhavan, Simha, Kaiser, Gail, Jebara, Tony.  2016.  Code Relatives: Detecting Similarly Behaving Software. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. :702–714.

Detecting “similar code” is useful for many software engineering tasks. Current tools can help detect code with statically similar syntactic and–or semantic features (code clones) and with dynamically similar functional input/output (simions). Unfortunately, some code fragments that behave similarly at the finer granularity of their execution traces may be ignored. In this paper, we propose the term “code relatives” to refer to code with similar execution behavior. We define code relatives and then present DyCLINK, our approach to detecting code relatives within and across codebases. DyCLINK records instruction-level traces from sample executions, organizes the traces into instruction-level dynamic dependence graphs, and employs our specialized subgraph matching algorithm to efficiently compare the executions of candidate code relatives. In our experiments, DyCLINK analyzed 422+ million prospective subgraph matches in only 43 minutes. We compared DyCLINK to one static code clone detector from the community and to our implementation of a dynamic simion detector. The results show that DyCLINK effectively detects code relatives with a reasonable analysis time.

Smith, Justin.  2016.  Identifying Successful Strategies for Resolving Static Analysis Notifications. Proceedings of the 38th International Conference on Software Engineering Companion. :662–664.

Although static analysis tools detect potential code defects early in the development process, they do not fully support developers in resolving those defects. To accurately and efficiently resolve defects, developers must orchestrate several complex tasks, such as determining whether the defect is a false positive and updating the source code without introducing new defects. Without good defect resolution strategies developers may resolve defects erroneously or inefficiently. In this work, I perform a preliminary analysis of the successful and unsuccessful strategies developers use to resolve defects. Based on the successful strategies identified, I then outline a tool to support developers throughout the defect resolution process.

Legunsen, Owolabi, Hariri, Farah, Shi, August, Lu, Yafeng, Zhang, Lingming, Marinov, Darko.  2016.  An Extensive Study of Static Regression Test Selection in Modern Software Evolution. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. :583–594.

Regression test selection (RTS) aims to reduce regression testing time by only re-running the tests affected by code changes. Prior research on RTS can be broadly split into dy namic and static techniques. A recently developed dynamic RTS technique called Ekstazi is gaining some adoption in practice, and its evaluation shows that selecting tests at a coarser, class-level granularity provides better results than selecting tests at a finer, method-level granularity. As dynamic RTS is gaining adoption, it is timely to also evaluate static RTS techniques, some of which were proposed over three decades ago but not extensively evaluated on modern software projects. This paper presents the first extensive study that evaluates the performance benefits of static RTS techniques and their safety; a technique is safe if it selects to run all tests that may be affected by code changes. We implemented two static RTS techniques, one class-level and one method-level, and compare several variants of these techniques. We also compare these static RTS techniques against Ekstazi, a state-of-the-art, class-level, dynamic RTS technique. The experimental results on 985 revisions of 22 open-source projects show that the class-level static RTS technique is comparable to Ekstazi, with similar performance benefits, but at the risk of being unsafe sometimes. In contrast, the method-level static RTS technique performs rather poorly.

Tymburibá, Mateus, Moreira, Rubens E. A., Quintão Pereira, Fernando Magno.  2016.  Inference of Peak Density of Indirect Branches to Detect ROP Attacks. Proceedings of the 2016 International Symposium on Code Generation and Optimization. :150–159.

A program subject to a Return-Oriented Programming (ROP) attack usually presents an execution trace with a high frequency of indirect branches. From this observation, several researchers have proposed to monitor the density of these instructions to detect ROP attacks. These techniques use universal thresholds: the density of indirect branches that characterizes an attack is the same for every application. This paper shows that universal thresholds are easy to circumvent. As an alternative, we introduce an inter-procedural semi-context-sensitive static code analysis that estimates the maximum density of indirect branches possible for a program. This analysis determines detection thresholds for each application; thus, making it more difficult for attackers to compromise programs via ROP. We have used an implementation of our technique in LLVM to find specific thresholds for the programs in SPEC CPU2006. By comparing these thresholds against actual execution traces of corresponding programs, we demonstrate the accuracy of our approach. Furthermore, our algorithm is practical: it finds an approximate solution to a theoretically undecidable problem, and handles programs with up to 700 thousand assembly instructions in 25 minutes.

Brown, Fraser, Nötzli, Andres, Engler, Dawson.  2016.  How to Build Static Checking Systems Using Orders of Magnitude Less Code. Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. :143–157.

Modern static bug finding tools are complex. They typically consist of hundreds of thousands of lines of code, and most of them are wedded to one language (or even one compiler). This complexity makes the systems hard to understand, hard to debug, and hard to retarget to new languages, thereby dramatically limiting their scope. This paper reduces checking system complexity by addressing a fundamental assumption, the assumption that checkers must depend on a full-blown language specification and compiler front end. Instead, our program checkers are based on drastically incomplete language grammars ("micro-grammars") that describe only portions of a language relevant to a checker. As a result, our implementation is tiny-roughly 2500 lines of code, about two orders of magnitude smaller than a typical system. We hope that this dramatic increase in simplicity will allow people to use more checkers on more systems in more languages. We implement our approach in μchex, a language-agnostic framework for writing static bug checkers. We use it to build micro-grammar based checkers for six languages (C, the C preprocessor, C++, Java, JavaScript, and Dart) and find over 700 errors in real-world projects.

Kumar, Snehasish, Srinivasan, Vijayalakshmi, Sharifian, Amirali, Sumner, Nick, Shriraman, Arrvindh.  2016.  Peruse and Profit: Estimating the Accelerability of Loops. Proceedings of the 2016 International Conference on Supercomputing. :21:1–21:13.

There exist a multitude of execution models available today for a developer to target. The choices vary from general purpose processors to fixed-function hardware accelerators with a large number of variations in-between. There is a growing demand to assess the potential benefits of porting or rewriting an application to a target architecture in order to fully exploit the benefits of performance and/or energy efficiency offered by such targets. However, as a first step of this process, it is necessary to determine whether the application has characteristics suitable for acceleration. In this paper, we present Peruse, a tool to characterize the features of loops in an application and to help the programmer understand the amenability of loops for acceleration. We consider a diverse set of features ranging from loop characteristics (e.g., loop exit points) and operation mixes (e.g., control vs data operations) to wider code region characteristics (e.g., idempotency, vectorizability). Peruse is language, architecture, and input independent and uses the intermediate representation of compilers to do the characterization. Using static analyses makes Peruse scalable and enables analysis of large applications to identify and extract interesting loops suitable for acceleration. We show analysis results for unmodified applications from the SPEC CPU benchmark suite, Polybench, and HPC workloads. For an end-user it is more desirable to get an estimate of the potential speedup due to acceleration. We use the workload characterization results of Peruse as features and develop a machine-learning based model to predict the potential speedup of a loop when off-loaded to a fixed function hardware accelerator. We use the model to predict the speedup of loops selected by Peruse and achieve an accuracy of 79%.

Wang, Bolun.  2016.  Defending Against Sybil Devices in Crowdsourced Mapping Services. Proceedings of on MobiSys 2016 PhD Forum. :3–4.

Crowdsourcing is an unique and practical approach to obtain personalized data and content. Its impact is especially significant in providing commentary, reviews and metadata, on a variety of location based services. In this study, we examine reliability of the Waze mapping service, and its vulnerability to a variety of location-based attacks. Our goals are to understand the severity of the problem, shed light on the general problem of location and device authentication, and explore the efficacy of potential defenses. Our preliminary results already show that a single attacker with limited resources can cause havoc on Waze, producing ``virtual'' congestion and accidents, automatically re-routing user traffic, and compromising user privacy by tracking users' precise movements via software while staying undetected. To defend against these attacks, we propose a proximity-based Sybil detection method to filter out malicious devices.

Adepu, Sridhar, Mathur, Aditya.  2016.  Distributed Detection of Single-Stage Multipoint Cyber Attacks in a Water Treatment Plant. Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security. :449–460.

A distributed detection method is proposed to detect single stage multi-point (SSMP) attacks on a Cyber Physical System (CPS). Such attacks aim at compromising two or more sensors or actuators at any one stage of a CPS and could totally compromise a controller and prevent it from detecting the attack. However, as demonstrated in this work, using the flow properties of water from one stage to the other, a neighboring controller was found effective in detecting such attacks. The method is based on physical invariants derived for each stage of the CPS from its design. The attack detection effectiveness of the method was evaluated experimentally against an operational water treatment testbed containing 42 sensors and actuators. Results from the experiments point to high effectiveness of the method in detecting a variety of SSMP attacks but also point to its limitations. Distributing the attack detection code among various controllers adds to the scalability of the proposed method.

Shrivastava, Aviral, Derler, Patricia, Baboud, Ya-Shian Li, Stanton, Kevin, Khayatian, Mohammad, Andrade, Hugo A., Weiss, Marc, Eidson, John, Chandhoke, Sundeep.  2016.  Time in Cyber-physical Systems. Proceedings of the Eleventh IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. :4:1–4:10.

Many modern cyber-physical systems (CPS), especially industrial automation systems, require the actions of multiple computational systems to be performed at much higher rates and more tightly synchronized than is possible with ad hoc designs. Time is the common entity that computing and physical systems in CPS share, and correct interfacing of that is essential to flawless functionality of a CPS. Fundamental research is needed on ways to synchronize clocks of computing systems to a high degree, and on design methods that enable building blocks of CPS to perform actions at specified times. To realize the potential of CPS in the coming decades, suitable ways to specify distributed CPS applications are needed, including their timing requirements, ways to specify the timing of the CPS components (e.g. sensors, actuators, computing platform), timing analysis to determine if the application design is possible using the components, confident top-down design methodologies that can ensure that the system meets its timing requirements, and ways and methodologies to test and verify that the system meets the timing requirements. Furthermore, strategies for securing timing need to be carefully considered at every CPS design stage and not simply added on. This paper exposes these challenges of CPS development, points out limitations of previous approaches, and provides some research directions towards solving these challenges.

Dutt, Nikil, Jantsch, Axel, Sarma, Santanu.  2016.  Toward Smart Embedded Systems: A Self-aware System-on-Chip (SoC) Perspective. ACM Trans. Embed. Comput. Syst.. 15:22:1–22:27.

Embedded systems must address a multitude of potentially conflicting design constraints such as resiliency, energy, heat, cost, performance, security, etc., all in the face of highly dynamic operational behaviors and environmental conditions. By incorporating elements of intelligence, the hope is that the resulting “smart” embedded systems will function correctly and within desired constraints in spite of highly dynamic changes in the applications and the environment, as well as in the underlying software/hardware platforms. Since terms related to “smartness” (e.g., self-awareness, self-adaptivity, and autonomy) have been used loosely in many software and hardware computing contexts, we first present a taxonomy of “self-x” terms and use this taxonomy to relate major “smart” software and hardware computing efforts. A major attribute for smart embedded systems is the notion of self-awareness that enables an embedded system to monitor its own state and behavior, as well as the external environment, so as to adapt intelligently. Toward this end, we use a System-on-Chip perspective to show how the CyberPhysical System-on-Chip (CPSoC) exemplar platform achieves self-awareness through a combination of cross-layer sensing, actuation, self-aware adaptations, and online learning. We conclude with some thoughts on open challenges and research directions.

Huang, Zhenqi, Wang, Yu, Mitra, Sayan, Dullerud, Geir.  2016.  Controller Synthesis for Linear Dynamical Systems with Adversaries. Proceedings of the Symposium and Bootcamp on the Science of Security. :53–62.

We present a controller synthesis algorithm for a reach-avoid problem in the presence of adversaries. Our model of the adversary abstractly captures typical malicious attacks envisioned on cyber-physical systems such as sensor spoofing, controller corruption, and actuator intrusion. After formulating the problem in a general setting, we present a sound and complete algorithm for the case with linear dynamics and an adversary with a budget on the total L2-norm of its actions. The algorithm relies on a result from linear control theory that enables us to decompose and compute the reachable states of the system in terms of a symbolic simulation of the adversary-free dynamics and the total uncertainty induced by the adversary. With this decomposition, the synthesis problem eliminates the universal quantifier on the adversary's choices and the symbolic controller actions can be effectively solved using an SMT solver. The constraints induced by the adversary are computed by solving second-order cone programmings. The algorithm is later extended to synthesize state-dependent controller and to generate attacks for the adversary. We present preliminary experimental results that show the effectiveness of this approach on several example problems.

Kang, Eunsuk, Adepu, Sridhar, Jackson, Daniel, Mathur, Aditya P..  2016.  Model-based Security Analysis of a Water Treatment System. Proceedings of the 2Nd International Workshop on Software Engineering for Smart Cyber-Physical Systems. :22–28.

An approach to analyzing the security of a cyber-physical system (CPS) is proposed, where the behavior of a physical plant and its controller are captured in approximate models, and their interaction is rigorously checked to discover potential attacks that involve a varying number of compromised sensors and actuators. As a preliminary study, this approach has been applied to a fully functional water treatment testbed constructed at the Singapore University of Technology and Design. The analysis revealed previously unknown attacks that were confirmed to pose serious threats to the safety of the testbed, and suggests a number of research challenges and opportunities for applying a similar type of formal analysis to cyber-physical security.

Wang, Kun, Du, Miao, Yang, Dejun, Zhu, Chunsheng, Shen, Jian, Zhang, Yan.  2016.  Game-Theory-Based Active Defense for Intrusion Detection in Cyber-Physical Embedded Systems. ACM Trans. Embed. Comput. Syst.. 16:18:1–18:21.

Cyber-Physical Embedded Systems (CPESs) are distributed embedded systems integrated with various actuators and sensors. When it comes to the issue of CPES security, the most significant problem is the security of Embedded Sensor Networks (ESNs). With the continuous growth of ESNs, the security of transferring data from sensors to their destinations has become an important research area. Due to the limitations in power, storage, and processing capabilities, existing security mechanisms for wired or wireless networks cannot apply directly to ESNs. Meanwhile, ESNs are likely to be attacked by different kinds of attacks in industrial scenarios. Therefore, there is a need to develop new techniques or modify the current security mechanisms to overcome these problems. In this article, we focus on Intrusion Detection (ID) techniques and propose a new attack-defense game model to detect malicious nodes using a repeated game approach. As a direct consequence of the game model, attackers and defenders make different strategies to achieve optimal payoffs. Importantly, error detection and missing detection are taken into consideration in Intrusion Detection Systems (IDSs), where a game tree model is introduced to solve this problem. In addition, we analyze and prove the existence of pure Nash equilibrium and mixed Nash equilibrium. Simulations show that the proposed model can both reduce energy consumption by up to 50% compared with the existing All Monitor (AM) model and improve the detection rate by up to 10% to 15% compared with the existing Cluster Head (CH) monitor model.

Ali, Sk Subidh, Ibrahim, Mohamed, Sinanoglu, Ozgur, Chakrabarty, Krishnendu, Karri, Ramesh.  2016.  Security Assessment of Cyberphysical Digital Microfluidic Biochips. IEEE/ACM Trans. Comput. Biol. Bioinformatics. 13:445–458.

A digital microfluidic biochip (DMFB) is an emerging technology that enables miniaturized analysis systems for point-of-care clinical diagnostics, DNA sequencing, and environmental monitoring. A DMFB reduces the rate of sample and reagent consumption, and automates the analysis of assays. In this paper, we provide the first assessment of the security vulnerabilities of DMFBs. We identify result-manipulation attacks on a DMFB that maliciously alter the assay outcomes. Two practical result-manipulation attacks are shown on a DMFB platform performing enzymatic glucose assay on serum. In the first attack, the attacker adjusts the concentration of the glucose sample and thereby modifies the final result. In the second attack, the attacker tampers with the calibration curve of the assay operation. We then identify denial-of-service attacks, where the attacker can disrupt the assay operation by tampering either with the droplet-routing algorithm or with the actuation sequence. We demonstrate these attacks using a digital microfluidic synthesis simulator. The results show that the attacks are easy to implement and hard to detect. Therefore, this work highlights the need for effective protections against malicious modifications in DMFBs.