-
Security Modelling for Cyber-Physical Systems: A Systematic Literature Review
Authors:
Shaofei Huang,
Christopher M. Poskitt,
Lwin Khin Shar
Abstract:
Cyber-physical systems (CPS) are at the intersection of digital technology and engineering domains, rendering them high-value targets of sophisticated and well-funded cybersecurity threat actors. Prominent cybersecurity attacks on CPS have brought attention to the vulnerability of these systems, and the soft underbelly of critical infrastructure reliant on CPS. Security modelling for CPS is an imp…
▽ More
Cyber-physical systems (CPS) are at the intersection of digital technology and engineering domains, rendering them high-value targets of sophisticated and well-funded cybersecurity threat actors. Prominent cybersecurity attacks on CPS have brought attention to the vulnerability of these systems, and the soft underbelly of critical infrastructure reliant on CPS. Security modelling for CPS is an important mechanism to systematically identify and assess vulnerabilities, threats, and risks throughout system lifecycles, and to ultimately ensure system resilience, safety, and reliability. This literature review delves into state-of-the-art research in CPS security modelling, encompassing both threat and attack modelling. While these terms are sometimes used interchangeably, they are different concepts. This article elaborates on the differences between threat and attack modelling, examining their implications for CPS security. A systematic search yielded 428 articles, from which 15 were selected and categorised into three clusters: those focused on threat modelling methods, attack modelling methods, and literature reviews. Specifically, we sought to examine what security modelling methods exist today, and how they address real-world cybersecurity threats and CPS-specific attacker capabilities throughout the lifecycle of CPS, which typically span longer durations compared to traditional IT systems. This article also highlights several limitations in existing research, wherein security models adopt simplistic approaches that do not adequately consider the dynamic, multi-layer, multi-path, and multi-agent characteristics of real-world cyber-physical attacks.
△ Less
Submitted 11 April, 2024;
originally announced April 2024.
-
ACAV: A Framework for Automatic Causality Analysis in Autonomous Vehicle Accident Recordings
Authors:
Huijia Sun,
Christopher M. Poskitt,
Yang Sun,
Jun Sun,
Yuqi Chen
Abstract:
The rapid progress of autonomous vehicles~(AVs) has brought the prospect of a driverless future closer than ever. Recent fatalities, however, have emphasized the importance of safety validation through large-scale testing. Multiple approaches achieve this fully automatically using high-fidelity simulators, i.e., by generating diverse driving scenarios and evaluating autonomous driving systems~(ADS…
▽ More
The rapid progress of autonomous vehicles~(AVs) has brought the prospect of a driverless future closer than ever. Recent fatalities, however, have emphasized the importance of safety validation through large-scale testing. Multiple approaches achieve this fully automatically using high-fidelity simulators, i.e., by generating diverse driving scenarios and evaluating autonomous driving systems~(ADSs) against different test oracles. While effective at finding violations, these approaches do not identify the decisions and actions that \emph{caused} them -- information that is critical for improving the safety of ADSs. To address this challenge, we propose ACAV, an automated framework designed to conduct causality analysis for AV accident recordings in two stages. First, we apply feature extraction schemas based on the messages exchanged between ADS modules, and use a weighted voting method to discard frames of the recording unrelated to the accident. Second, we use safety specifications to identify safety-critical frames and deduce causal events by applying CAT -- our causal analysis tool -- to a station-time graph. We evaluate ACAV on the Apollo ADS, finding that it can identify five distinct types of causal events in 93.64% of 110 accident recordings generated by an AV testing engine. We further evaluated ACAV on 1206 accident recordings collected from versions of Apollo injected with specific faults, finding that it can correctly identify causal events in 96.44% of the accidents triggered by prediction errors, and 85.73% of the accidents triggered by planning errors.
△ Less
Submitted 13 January, 2024;
originally announced January 2024.
-
REDriver: Runtime Enforcement for Autonomous Vehicles
Authors:
Yang Sun,
Christopher M. Poskitt,
Xiaodong Zhang,
Jun Sun
Abstract:
Autonomous driving systems (ADSs) integrate sensing, perception, drive control, and several other critical tasks in autonomous vehicles, motivating research into techniques for assessing their safety. While there are several approaches for testing and analysing them in high-fidelity simulators, ADSs may still encounter additional critical scenarios beyond those covered once they are deployed on re…
▽ More
Autonomous driving systems (ADSs) integrate sensing, perception, drive control, and several other critical tasks in autonomous vehicles, motivating research into techniques for assessing their safety. While there are several approaches for testing and analysing them in high-fidelity simulators, ADSs may still encounter additional critical scenarios beyond those covered once they are deployed on real roads. An additional level of confidence can be established by monitoring and enforcing critical properties when the ADS is running. Existing work, however, is only able to monitor simple safety properties (e.g., avoidance of collisions) and is limited to blunt enforcement mechanisms such as hitting the emergency brakes. In this work, we propose REDriver, a general and modular approach to runtime enforcement, in which users can specify a broad range of properties (e.g., national traffic laws) in a specification language based on signal temporal logic (STL). REDriver monitors the planned trajectory of the ADS based on a quantitative semantics of STL, and uses a gradient-driven algorithm to repair the trajectory when a violation of the specification is likely. We implemented REDriver for two versions of Apollo (i.e., a popular ADS), and subjected it to a benchmark of violations of Chinese traffic laws. The results show that REDriver significantly improves Apollo's conformance to the specification with minimal overhead.
△ Less
Submitted 4 January, 2024;
originally announced January 2024.
-
Fixing Your Own Smells: Adding a Mistake-Based Familiarisation Step When Teaching Code Refactoring
Authors:
Ivan Tan,
Christopher M. Poskitt
Abstract:
Programming problems can be solved in a multitude of functionally correct ways, but the quality of these solutions (e.g. readability, maintainability) can vary immensely. When code quality is poor, symptoms emerge in the form of 'code smells', which are specific negative characteristics (e.g. duplicate code) that can be resolved by applying refactoring patterns. Many undergraduate computing curric…
▽ More
Programming problems can be solved in a multitude of functionally correct ways, but the quality of these solutions (e.g. readability, maintainability) can vary immensely. When code quality is poor, symptoms emerge in the form of 'code smells', which are specific negative characteristics (e.g. duplicate code) that can be resolved by applying refactoring patterns. Many undergraduate computing curricula train students on this software engineering practice, often doing so via exercises on unfamiliar instructor-provided code. Our observation, however, is that this makes it harder for novices to internalise refactoring as part of their own development practices. In this paper, we propose a new approach to teaching refactoring, in which students must first complete a programming exercise constrained to ensure they will produce a code smell. This simple intervention is based on the idea that learning refactoring is easier if students are familiar with the code (having built it), that it brings refactoring closer to their regular development practice, and that it presents a powerful opportunity to learn from a 'mistake'. We designed and conducted a study with 35 novice undergraduates in which they completed various refactoring exercises alternately taught using a traditional and our 'mistake-based' approach, finding that students were significantly more effective and confident at completing exercises using the latter.
△ Less
Submitted 1 January, 2024;
originally announced January 2024.
-
How Helpful do Novice Programmers Find the Feedback of an Automated Repair Tool?
Authors:
Oka Kurniawan,
Christopher M. Poskitt,
Ismam Al Hoque,
Norman Tiong Seng Lee,
Cyrille Jégourel,
Nachamma Sockalingam
Abstract:
Immediate feedback has been shown to improve student learning. In programming courses, immediate, automated feedback is typically provided in the form of pre-defined test cases run by a submission platform. While these are excellent for highlighting the presence of logical errors, they do not provide novice programmers enough scaffolding to help them identify where an error is or how to fix it. To…
▽ More
Immediate feedback has been shown to improve student learning. In programming courses, immediate, automated feedback is typically provided in the form of pre-defined test cases run by a submission platform. While these are excellent for highlighting the presence of logical errors, they do not provide novice programmers enough scaffolding to help them identify where an error is or how to fix it. To address this, several tools have been developed that provide richer feedback in the form of program repairs. Studies of such tools, however, tend to focus more on whether correct repairs can be generated, rather than how novices are using them. In this paper, we describe our experience of using CLARA, an automated repair tool, to provide feedback to novices. First, we extended CLARA to support a larger subset of the Python language, before integrating it with the Jupyter Notebooks used for our programming exercises. Second, we devised a preliminary study in which students tackled programming problems with and without support of the tool using the 'think aloud' protocol. We found that novices often struggled to understand the proposed repairs, echoing the well-known challenge to understand compiler/interpreter messages. Furthermore, we found that students valued being told where a fix was needed - without necessarily the fix itself - suggesting that 'less may be more' from a pedagogical perspective.
△ Less
Submitted 7 October, 2023; v1 submitted 2 October, 2023;
originally announced October 2023.
-
How Generalizable are Deepfake Detectors? An Empirical Study
Authors:
Boquan Li,
Jun Sun,
Christopher M. Poskitt
Abstract:
Deepfake videos and images are becoming increasingly credible, posing a significant threat given their potential to facilitate fraud or bypass access control systems. This has motivated the development of deepfake detection methods, in which deep learning models are trained to distinguish between real and synthesized footage. Unfortunately, existing detection models struggle to generalize to deepf…
▽ More
Deepfake videos and images are becoming increasingly credible, posing a significant threat given their potential to facilitate fraud or bypass access control systems. This has motivated the development of deepfake detection methods, in which deep learning models are trained to distinguish between real and synthesized footage. Unfortunately, existing detection models struggle to generalize to deepfakes from datasets they were not trained on, but little work has been done to examine why or how this limitation can be addressed. In this paper, we present the first empirical study on the generalizability of deepfake detectors, an essential goal for detectors to stay one step ahead of attackers. Our study utilizes six deepfake datasets, five deepfake detection methods, and two model augmentation approaches, confirming that detectors do not generalize in zero-shot settings. Additionally, we find that detectors are learning unwanted properties specific to synthesis methods and struggling to extract discriminative features, limiting their ability to generalize. Finally, we find that there are neurons universally contributing to detection across seen and unseen datasets, illuminating a possible path forward to zero-shot generalizability.
△ Less
Submitted 8 August, 2023;
originally announced August 2023.
-
Finding Causally Different Tests for an Industrial Control System
Authors:
Christopher M. Poskitt,
Yuqi Chen,
Jun Sun,
Yu Jiang
Abstract:
Industrial control systems (ICSs) are types of cyber-physical systems in which programs, written in languages such as ladder logic or structured text, control industrial processes through sensing and actuating. Given the use of ICSs in critical infrastructure, it is important to test their resilience against manipulations of sensor/actuator inputs. Unfortunately, existing methods fail to test them…
▽ More
Industrial control systems (ICSs) are types of cyber-physical systems in which programs, written in languages such as ladder logic or structured text, control industrial processes through sensing and actuating. Given the use of ICSs in critical infrastructure, it is important to test their resilience against manipulations of sensor/actuator inputs. Unfortunately, existing methods fail to test them comprehensively, as they typically focus on finding the simplest-to-craft manipulations for a testing goal, and are also unable to determine when a test is simply a minor permutation of another, i.e. based on the same causal events. In this work, we propose a guided fuzzing approach for finding 'meaningfully different' tests for an ICS via a general formalisation of sensor/actuator-manipulation strategies. Our algorithm identifies the causal events in a test, generalises them to an equivalence class, and then updates the fuzzing strategy so as to find new tests that are causally different from those already identified. An evaluation of our approach on a real-world water treatment system shows that it is able to find 106% more causally different tests than the most comparable fuzzer. While we focus on diversifying the test suite of an ICS, our formalisation may be useful for other fuzzers that intercept communication channels.
△ Less
Submitted 10 February, 2023; v1 submitted 8 February, 2023;
originally announced February 2023.
-
Proceedings of the Thirteenth International Workshop on Graph Computation Models
Authors:
Reiko Heckel,
Christopher M. Poskitt
Abstract:
This volume contains the post-proceedings of the Thirteenth International Workshop on Graph Computation Models (GCM 2022). The workshop took place in Nantes, France on 6th July 2022 as part of STAF 2022 (Software Technologies: Applications and Foundations). Graphs are common mathematical structures that are visual and intuitive. They constitute a natural and seamless way for system modelling in sc…
▽ More
This volume contains the post-proceedings of the Thirteenth International Workshop on Graph Computation Models (GCM 2022). The workshop took place in Nantes, France on 6th July 2022 as part of STAF 2022 (Software Technologies: Applications and Foundations). Graphs are common mathematical structures that are visual and intuitive. They constitute a natural and seamless way for system modelling in science, engineering, and beyond, including computer science, biology, and business process modelling. Graph computation models constitute a class of very high-level models where graphs are first-class citizens. The aim of the International GCM Workshop series is to bring together researchers interested in all aspects of computation models based on graphs and graph transformation. It promotes the cross-fertilising exchange of ideas and experiences among senior and young researchers from the different communities interested in the foundations, applications, and implementations of graph computation models and related areas.
△ Less
Submitted 21 December, 2022;
originally announced December 2022.
-
LawBreaker: An Approach for Specifying Traffic Laws and Fuzzing Autonomous Vehicles
Authors:
Yang Sun,
Christopher M. Poskitt,
Jun Sun,
Yuqi Chen,
Zijiang Yang
Abstract:
Autonomous driving systems (ADSs) must be tested thoroughly before they can be deployed in autonomous vehicles. High-fidelity simulators allow them to be tested against diverse scenarios, including those that are difficult to recreate in real-world testing grounds. While previous approaches have shown that test cases can be generated automatically, they tend to focus on weak oracles (e.g. reaching…
▽ More
Autonomous driving systems (ADSs) must be tested thoroughly before they can be deployed in autonomous vehicles. High-fidelity simulators allow them to be tested against diverse scenarios, including those that are difficult to recreate in real-world testing grounds. While previous approaches have shown that test cases can be generated automatically, they tend to focus on weak oracles (e.g. reaching the destination without collisions) without assessing whether the journey itself was undertaken safely and satisfied the law. In this work, we propose LawBreaker, an automated framework for testing ADSs against real-world traffic laws, which is designed to be compatible with different scenario description languages. LawBreaker provides a rich driver-oriented specification language for describing traffic laws, and a fuzzing engine that searches for different ways of violating them by maximising specification coverage. To evaluate our approach, we implemented it for Apollo+LGSVL and specified the traffic laws of China. LawBreaker was able to find 14 violations of these laws, including 173 test cases that caused accidents.
△ Less
Submitted 24 October, 2022; v1 submitted 31 August, 2022;
originally announced August 2022.
-
XSS for the Masses: Integrating Security in a Web Programming Course using a Security Scanner
Authors:
Lwin Khin Shar,
Christopher M. Poskitt,
Kyong ** Shim,
Li Ying Leonard Wong
Abstract:
Cybersecurity education is considered an important part of undergraduate computing curricula, but many institutions teach it only in dedicated courses or tracks. This optionality risks students graduating with limited exposure to secure coding practices that are expected in industry. An alternative approach is to integrate cybersecurity concepts across non-security courses, so as to expose student…
▽ More
Cybersecurity education is considered an important part of undergraduate computing curricula, but many institutions teach it only in dedicated courses or tracks. This optionality risks students graduating with limited exposure to secure coding practices that are expected in industry. An alternative approach is to integrate cybersecurity concepts across non-security courses, so as to expose students to the interplay between security and other sub-areas of computing. In this paper, we report on our experience of applying the security integration approach to an undergraduate web programming course. In particular, we added a practical introduction to secure coding, which highlighted the OWASP Top 10 vulnerabilities by example, and demonstrated how to identify them using out-of-the-box security scanner tools (e.g. ZAP). Furthermore, we incentivised students to utilise these tools in their own course projects by offering bonus marks. To assess the impact of this intervention, we scanned students' project code over the last three years, finding a reduction in the number of vulnerabilities. Finally, in focus groups and a survey, students shared that our intervention helped to raise awareness, but they also highlighted the importance of grading incentives and the need to teach security content earlier.
△ Less
Submitted 26 April, 2022;
originally announced April 2022.
-
K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs
Authors:
Kun Wang,
**gyi Wang,
Christopher M. Poskitt,
Xiangxiang Chen,
Jun Sun,
Peng Cheng
Abstract:
Programmable Logic Controllers (PLCs) are responsible for automating process control in many industrial systems (e.g. in manufacturing and public infrastructure), and thus it is critical to ensure that they operate correctly and safely. The majority of PLCs are programmed in languages such as Structured Text (ST). However, a lack of formal semantics makes it difficult to ascertain the correctness…
▽ More
Programmable Logic Controllers (PLCs) are responsible for automating process control in many industrial systems (e.g. in manufacturing and public infrastructure), and thus it is critical to ensure that they operate correctly and safely. The majority of PLCs are programmed in languages such as Structured Text (ST). However, a lack of formal semantics makes it difficult to ascertain the correctness of their translators and compilers, which vary from vendor-to-vendor. In this work, we develop K-ST, a formal executable semantics for ST in the K framework. Defined with respect to the IEC 61131-3 standard and PLC vendor manuals, K-ST is a high-level reference semantics that can be used to evaluate the correctness and consistency of different ST implementations. We validate K-ST by executing 509 ST programs extracted from Github and comparing the results against existing commercial compilers (i.e., CODESYS, CX-Programmer, and GX Works2). We then apply K-ST to validate the implementation of the open source OpenPLC platform, comparing the executions of several test programs to uncover five bugs and nine functional defects in the compiler.
△ Less
Submitted 11 September, 2023; v1 submitted 8 February, 2022;
originally announced February 2022.
-
Mind the Gap: Reimagining an Interactive Programming Course for the Synchronous Hybrid Classroom
Authors:
Christopher M. Poskitt,
Kyong ** Shim,
Yi Meng Lau,
Hong Seng Ong
Abstract:
COVID-19 has significantly affected universities, forcing many courses to be delivered entirely online. As countries bring the pandemic under control, a potential way to safely resume some face-to-face teaching is the synchronous hybrid classroom, in which physically and remotely attending students are taught simultaneously. This comes with challenges, however, including the risk that remotely att…
▽ More
COVID-19 has significantly affected universities, forcing many courses to be delivered entirely online. As countries bring the pandemic under control, a potential way to safely resume some face-to-face teaching is the synchronous hybrid classroom, in which physically and remotely attending students are taught simultaneously. This comes with challenges, however, including the risk that remotely attending students perceive a 'gap' between their engagement and that of their physical peers. In this experience report, we describe how an interactive programming course was adapted to hybrid delivery in a way that mitigated this risk. Our solution centred on the use of a professional communication platform - Slack - to equalise participation opportunities and to facilitate peer learning. Furthermore, to mitigate 'Zoom fatigue', we implemented a semi-flipped classroom, covering concepts in videos and using shorter lessons to consolidate them. Finally, we critically reflect on the results of a student survey and our own experiences of implementing the solution.
△ Less
Submitted 19 September, 2021;
originally announced September 2021.
-
Steps Before Syntax: Hel** Novice Programmers Solve Problems using the PCDIT Framework
Authors:
Oka Kurniawan,
Cyrille Jégourel,
Norman Tiong Seng Lee,
Matthieu De Mari,
Christopher M. Poskitt
Abstract:
Novice programmers often struggle with problem solving due to the high cognitive loads they face. Furthermore, many introductory programming courses do not explicitly teach it, assuming that problem solving skills are acquired along the way. In this paper, we present 'PCDIT', a non-linear problem solving framework that provides scaffolding to guide novice programmers through the process of transfo…
▽ More
Novice programmers often struggle with problem solving due to the high cognitive loads they face. Furthermore, many introductory programming courses do not explicitly teach it, assuming that problem solving skills are acquired along the way. In this paper, we present 'PCDIT', a non-linear problem solving framework that provides scaffolding to guide novice programmers through the process of transforming a problem specification into an implemented and tested solution for an imperative programming language. A key distinction of PCDIT is its focus on develo** concrete cases for the problem early without actually writing test code: students are instead encouraged to think about the abstract steps from inputs to outputs before map** anything down to syntax. We reflect on our experience of teaching an introductory programming course using PCDIT, and report the results of a survey that suggests it helped students to break down challenging problems, organise their thoughts, and reach working solutions.
△ Less
Submitted 18 September, 2021;
originally announced September 2021.
-
Code Integrity Attestation for PLCs using Black Box Neural Network Predictions
Authors:
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun
Abstract:
Cyber-physical systems (CPSs) are widespread in critical domains, and significant damage can be caused if an attacker is able to modify the code of their programmable logic controllers (PLCs). Unfortunately, traditional techniques for attesting code integrity (i.e. verifying that it has not been modified) rely on firmware access or roots-of-trust, neither of which proprietary or legacy PLCs are li…
▽ More
Cyber-physical systems (CPSs) are widespread in critical domains, and significant damage can be caused if an attacker is able to modify the code of their programmable logic controllers (PLCs). Unfortunately, traditional techniques for attesting code integrity (i.e. verifying that it has not been modified) rely on firmware access or roots-of-trust, neither of which proprietary or legacy PLCs are likely to provide. In this paper, we propose a practical code integrity checking solution based on privacy-preserving black box models that instead attest the input/output behaviour of PLC programs. Using faithful offline copies of the PLC programs, we identify their most important inputs through an information flow analysis, execute them on multiple combinations to collect data, then train neural networks able to predict PLC outputs (i.e. actuator commands) from their inputs. By exploiting the black box nature of the model, our solution maintains the privacy of the original PLC code and does not assume that attackers are unaware of its presence. The trust instead comes from the fact that it is extremely hard to attack the PLC code and neural networks at the same time and with consistent outcomes. We evaluated our approach on a modern six-stage water treatment plant testbed, finding that it could predict actuator states from PLC inputs with near-100% accuracy, and thus could detect all 120 effective code mutations that we subjected the PLCs to. Finally, we found that it is not practically possible to simultaneously modify the PLC code and apply discreet adversarial noise to our attesters in a way that leads to consistent (mis-)predictions.
△ Less
Submitted 17 July, 2021; v1 submitted 14 June, 2021;
originally announced June 2021.
-
Adversarial Attacks and Mitigation for Anomaly Detectors of Cyber-Physical Systems
Authors:
Yifan Jia,
**gyi Wang,
Christopher M. Poskitt,
Sudipta Chattopadhyay,
Jun Sun,
Yuqi Chen
Abstract:
The threats faced by cyber-physical systems (CPSs) in critical infrastructure have motivated research into a multitude of attack detection mechanisms, including anomaly detectors based on neural network models. The effectiveness of anomaly detectors can be assessed by subjecting them to test suites of attacks, but less consideration has been given to adversarial attackers that craft noise specific…
▽ More
The threats faced by cyber-physical systems (CPSs) in critical infrastructure have motivated research into a multitude of attack detection mechanisms, including anomaly detectors based on neural network models. The effectiveness of anomaly detectors can be assessed by subjecting them to test suites of attacks, but less consideration has been given to adversarial attackers that craft noise specifically designed to deceive them. While successfully applied in domains such as images and audio, adversarial attacks are much harder to implement in CPSs due to the presence of other built-in defence mechanisms such as rule checkers(or invariant checkers). In this work, we present an adversarial attack that simultaneously evades the anomaly detectors and rule checkers of a CPS. Inspired by existing gradient-based approaches, our adversarial attack crafts noise over the sensor and actuator values, then uses a genetic algorithm to optimise the latter, ensuring that the neural network and the rule checking system are both deceived.We implemented our approach for two real-world critical infrastructure testbeds, successfully reducing the classification accuracy of their detectors by over 50% on average, while simultaneously avoiding detection by rule checkers. Finally, we explore whether these attacks can be mitigated by training the detectors on adversarial samples.
△ Less
Submitted 22 May, 2021;
originally announced May 2021.
-
Incorrectness Logic for Graph Programs
Authors:
Christopher M. Poskitt
Abstract:
Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and sho…
▽ More
Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this incorrectness logic to be sound and complete, and speculate on some possible future applications of it.
△ Less
Submitted 13 March, 2022; v1 submitted 10 May, 2021;
originally announced May 2021.
-
Towards Systematically Deriving Defence Mechanisms from Functional Requirements of Cyber-Physical Systems
Authors:
Cheah Huei Yoong,
Venkata Reddy Palleti,
Arlindo Silva,
Christopher M. Poskitt
Abstract:
The threats faced by cyber-physical systems (CPSs) in critical infrastructure have motivated the development of different attack detection mechanisms, such as those that monitor for violations of invariants, i.e. properties that always hold in normal operation. Given the complexity of CPSs, several existing approaches focus on deriving invariants automatically from data logs, but these can miss po…
▽ More
The threats faced by cyber-physical systems (CPSs) in critical infrastructure have motivated the development of different attack detection mechanisms, such as those that monitor for violations of invariants, i.e. properties that always hold in normal operation. Given the complexity of CPSs, several existing approaches focus on deriving invariants automatically from data logs, but these can miss possible system behaviours if they are not represented in that data. Furthermore, resolving any design flaws identified in this process is costly, as the CPS is already built. In this position paper, we propose a systematic method for deriving invariants before a CPS is built by analysing its functional requirements. Our method, inspired by the axiomatic design methodology for systems, iteratively analyses dependencies in the design to construct equations and process graphs that model the invariant relationships between CPS components. As a preliminary study, we applied it to the design of a water treatment plant testbed, implementing checkers for two invariants by using decision trees, and finding that they could detect some examples of attacks on the testbed with high accuracy and without false positives. Finally, we explore how develo** our method further could lead to more robust CPSs and reduced costs by identifying design weaknesses before systems are implemented.
△ Less
Submitted 25 September, 2020; v1 submitted 7 July, 2020;
originally announced July 2020.
-
Active Fuzzing for Testing and Securing Cyber-Physical Systems
Authors:
Yuqi Chen,
Bohan Xuan,
Christopher M. Poskitt,
Jun Sun,
Fan Zhang
Abstract:
Cyber-physical systems (CPSs) in critical infrastructure face a pervasive threat from attackers, motivating research into a variety of countermeasures for securing them. Assessing the effectiveness of these countermeasures is challenging, however, as realistic benchmarks of attacks are difficult to manually construct, blindly testing is ineffective due to the enormous search spaces and resource re…
▽ More
Cyber-physical systems (CPSs) in critical infrastructure face a pervasive threat from attackers, motivating research into a variety of countermeasures for securing them. Assessing the effectiveness of these countermeasures is challenging, however, as realistic benchmarks of attacks are difficult to manually construct, blindly testing is ineffective due to the enormous search spaces and resource requirements, and intelligent fuzzing approaches require impractical amounts of data and network access. In this work, we propose active fuzzing, an automatic approach for finding test suites of packet-level CPS network attacks, targeting scenarios in which attackers can observe sensors and manipulate packets, but have no existing knowledge about the payload encodings. Our approach learns regression models for predicting sensor values that will result from sampled network packets, and uses these predictions to guide a search for payload manipulations (i.e. bit flips) most likely to drive the CPS into an unsafe state. Key to our solution is the use of online active learning, which iteratively updates the models by sampling payloads that are estimated to maximally improve them. We evaluate the efficacy of active fuzzing by implementing it for a water purification plant testbed, finding it can automatically discover a test suite of flow, pressure, and over/underflow attacks, all with substantially less time, data, and network access than the most comparable approach. Finally, we demonstrate that our prediction models can also be utilised as countermeasures themselves, implementing them as anomaly detectors and early warning systems.
△ Less
Submitted 16 July, 2020; v1 submitted 28 May, 2020;
originally announced May 2020.
-
Securing Bring-Your-Own-Device (BYOD) Programming Exams
Authors:
Oka Kurniawan,
Norman Tiong Seng Lee,
Christopher M. Poskitt
Abstract:
Traditional pen and paper exams are inadequate for modern university programming courses as they are misaligned with pedagogies and learning objectives that target practical coding ability. Unfortunately, many institutions lack the resources or space to be able to run assessments in dedicated computer labs. This has motivated the development of bring-your-own-device (BYOD) exam formats, allowing s…
▽ More
Traditional pen and paper exams are inadequate for modern university programming courses as they are misaligned with pedagogies and learning objectives that target practical coding ability. Unfortunately, many institutions lack the resources or space to be able to run assessments in dedicated computer labs. This has motivated the development of bring-your-own-device (BYOD) exam formats, allowing students to program in a similar environment to how they learnt, but presenting instructors with significant additional challenges in preventing plagiarism and cheating. In this paper, we describe a BYOD exam solution based on lockdown browsers, software which temporarily turns students' laptops into secure workstations with limited system or internet access. We combine the use of this technology with a learning management system and cloud-based programming tool to facilitate conceptual and practical programming questions that can be tackled in an interactive but controlled environment. We reflect on our experience of implementing this solution for a major undergraduate programming course, highlighting our principal lesson that policies and support mechanisms are as important to consider as the technology itself.
△ Less
Submitted 12 January, 2020;
originally announced January 2020.
-
Learning-Guided Network Fuzzing for Testing Cyber-Physical System Defences
Authors:
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun,
Sridhar Adepu,
Fan Zhang
Abstract:
The threat of attack faced by cyber-physical systems (CPSs), especially when they play a critical role in automating public infrastructure, has motivated research into a wide variety of attack defence mechanisms. Assessing their effectiveness is challenging, however, as realistic sets of attacks to test them against are not always available. In this paper, we propose smart fuzzing, an automated, m…
▽ More
The threat of attack faced by cyber-physical systems (CPSs), especially when they play a critical role in automating public infrastructure, has motivated research into a wide variety of attack defence mechanisms. Assessing their effectiveness is challenging, however, as realistic sets of attacks to test them against are not always available. In this paper, we propose smart fuzzing, an automated, machine learning guided technique for systematically finding 'test suites' of CPS network attacks, without requiring any knowledge of the system's control programs or physical processes. Our approach uses predictive machine learning models and metaheuristic search algorithms to guide the fuzzing of actuators so as to drive the CPS into different unsafe physical states. We demonstrate the efficacy of smart fuzzing by implementing it for two real-world CPS testbeds---a water purification plant and a water distribution system---finding attacks that drive them into 27 different unsafe states involving water flow, pressure, and tank levels, including six that were not covered by an established attack benchmark. Finally, we use our approach to test the effectiveness of an invariant-based defence system for the water treatment plant, finding two attacks that were not detected by its physical invariant checks, highlighting a potential weakness that could be exploited in certain conditions.
△ Less
Submitted 11 September, 2019;
originally announced September 2019.
-
Learning from Mutants: Using Code Mutation to Learn and Monitor Invariants of a Cyber-Physical System
Authors:
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun
Abstract:
Cyber-physical systems (CPS) consist of sensors, actuators, and controllers all communicating over a network; if any subset becomes compromised, an attacker could cause significant damage. With access to data logs and a model of the CPS, the physical effects of an attack could potentially be detected before any damage is done. Manually building a model that is accurate enough in practice, however,…
▽ More
Cyber-physical systems (CPS) consist of sensors, actuators, and controllers all communicating over a network; if any subset becomes compromised, an attacker could cause significant damage. With access to data logs and a model of the CPS, the physical effects of an attack could potentially be detected before any damage is done. Manually building a model that is accurate enough in practice, however, is extremely difficult. In this paper, we propose a novel approach for constructing models of CPS automatically, by applying supervised machine learning to data traces obtained after systematically seeding their software components with faults ("mutants"). We demonstrate the efficacy of this approach on the simulator of a real-world water purification plant, presenting a framework that automatically generates mutants, collects data traces, and learns an SVM-based model. Using cross-validation and statistical model checking, we show that the learnt model characterises an invariant physical property of the system. Furthermore, we demonstrate the usefulness of the invariant by subjecting the system to 55 network and code-modification attacks, and showing that it can detect 85% of them from the data logs generated at runtime.
△ Less
Submitted 13 June, 2018; v1 submitted 3 January, 2018;
originally announced January 2018.
-
A Semantics Comparison Workbench for a Concurrent, Asynchronous, Distributed Programming Language
Authors:
Claudio Corrodi,
Alexander Heußner,
Christopher M. Poskitt
Abstract:
A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time---whether to improve performance, or to extend them to new language features---potentially affecting behavioural and safety properties of existing programs…
▽ More
A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time---whether to improve performance, or to extend them to new language features---potentially affecting behavioural and safety properties of existing programs. This is exemplified by SCOOP, a message-passing approach to concurrent object-oriented programming that has seen multiple changes proposed and implemented, with demonstrable consequences for an idiomatic usage of its core abstraction. We propose a semantics comparison workbench for SCOOP with fully and semi-automatic tools for analysing and comparing the state spaces of programs with respect to different execution models or semantics. We demonstrate its use in checking the consistency of properties across semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models of SCOOP. Furthermore, we demonstrate the extensibility of the workbench by generalising the formalisation of an execution model to support recently proposed extensions for distributed programming. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in the GROOVE tool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, how the visual yet algebraic nature of the model can be used to ascertain soundness, and highlight how the approach could be applied to similar languages.
△ Less
Submitted 11 October, 2017;
originally announced October 2017.
-
Anomaly Detection for a Water Treatment System Using Unsupervised Machine Learning
Authors:
Jun Inoue,
Yoriyuki Yamagata,
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun
Abstract:
In this paper, we propose and evaluate the application of unsupervised machine learning to anomaly detection for a Cyber-Physical System (CPS). We compare two methods: Deep Neural Networks (DNN) adapted to time series data generated by a CPS, and one-class Support Vector Machines (SVM). These methods are evaluated against data from the Secure Water Treatment (SWaT) testbed, a scaled-down but fully…
▽ More
In this paper, we propose and evaluate the application of unsupervised machine learning to anomaly detection for a Cyber-Physical System (CPS). We compare two methods: Deep Neural Networks (DNN) adapted to time series data generated by a CPS, and one-class Support Vector Machines (SVM). These methods are evaluated against data from the Secure Water Treatment (SWaT) testbed, a scaled-down but fully operational raw water purification plant. For both methods, we first train detectors using a log generated by SWaT operating under normal conditions. Then, we evaluate the performance of both methods using a log generated by SWaT operating under 36 different attack scenarios. We find that our DNN generates fewer false positives than our one-class SVM while our SVM detects slightly more anomalies. Overall, our DNN has a slightly better F measure than our SVM. We discuss the characteristics of the DNN and one-class SVM used in this experiment, and compare the advantages and disadvantages of the two methods.
△ Less
Submitted 25 September, 2017; v1 submitted 15 September, 2017;
originally announced September 2017.
-
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Authors:
Yuqi Chen,
Christopher M. Poskitt,
Jun Sun
Abstract:
Cyber-physical systems (CPS), which integrate algorithmic control with physical processes, often consist of physically distributed components communicating over a network. A malfunctioning or compromised component in such a CPS can lead to costly consequences, especially in the context of public infrastructure. In this short paper, we argue for the importance of constructing invariants (or models)…
▽ More
Cyber-physical systems (CPS), which integrate algorithmic control with physical processes, often consist of physically distributed components communicating over a network. A malfunctioning or compromised component in such a CPS can lead to costly consequences, especially in the context of public infrastructure. In this short paper, we argue for the importance of constructing invariants (or models) of the physical behaviour exhibited by CPS, motivated by their applications to the control, monitoring, and attestation of components. To achieve this despite the inherent complexity of CPS, we propose a new technique for learning invariants that combines machine learning with ideas from mutation testing. We present a preliminary study on a water treatment system that suggests the efficacy of this approach, propose strategies for establishing confidence in the correctness of invariants, then summarise some research questions and the steps we are taking to investigate them.
△ Less
Submitted 6 September, 2016;
originally announced September 2016.
-
An Interference-Free Programming Model for Network Objects
Authors:
Mischael Schill,
Christopher M. Poskitt,
Bertrand Meyer
Abstract:
Network objects are a simple and natural abstraction for distributed object-oriented programming. Languages that support network objects, however, often leave synchronization to the user, along with its associated pitfalls, such as data races and the possibility of failure. In this paper, we present D-SCOOP, a distributed programming model that allows for interference-free and transaction-like rea…
▽ More
Network objects are a simple and natural abstraction for distributed object-oriented programming. Languages that support network objects, however, often leave synchronization to the user, along with its associated pitfalls, such as data races and the possibility of failure. In this paper, we present D-SCOOP, a distributed programming model that allows for interference-free and transaction-like reasoning on (potentially multiple) network objects, with synchronization handled automatically, and network failures managed by a compensation mechanism. We achieve this by leveraging the runtime semantics of a multi-threaded object-oriented concurrency model, directly generalizing it with a message-based protocol for efficiently coordinating remote objects. We present our pathway to fusing these contrasting but complementary ideas, and evaluate the performance overhead of the automatic synchronization in D-SCOOP, finding that it comes close to---or outperforms---explicit locking-based synchronization in Java RMI.
△ Less
Submitted 15 April, 2016;
originally announced April 2016.
-
A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs
Authors:
Claudio Corrodi,
Alexander Heußner,
Christopher M. Poskitt
Abstract:
A number of novel programming languages and libraries have been proposed that offer simpler-to-use models of concurrency than threads. It is challenging, however, to devise execution models that successfully realise their abstractions without forfeiting performance or introducing unintended behaviours. This is exemplified by SCOOP---a concurrent object-oriented message-passing language---which has…
▽ More
A number of novel programming languages and libraries have been proposed that offer simpler-to-use models of concurrency than threads. It is challenging, however, to devise execution models that successfully realise their abstractions without forfeiting performance or introducing unintended behaviours. This is exemplified by SCOOP---a concurrent object-oriented message-passing language---which has seen multiple semantics proposed and implemented over its evolution. We propose a "semantics workbench" with fully and semi-automatic tools for SCOOP, that can be used to analyse and compare programs with respect to different execution models. We demonstrate its use in checking the consistency of semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models of the language. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in the GROOVE tool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, and how the visual yet algebraic nature of the model can be used to ascertain soundness.
△ Less
Submitted 1 March, 2016;
originally announced March 2016.
-
The AutoProof Verifier: Usability by Non-Experts and on Standard Code
Authors:
Carlo A. Furia,
Christopher M. Poskitt,
Julian Tschannen
Abstract:
Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof…
▽ More
Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof in two contrasting contexts representative of non-expert usage. First, we discuss its usability by students in a graduate course on software verification, who were tasked with verifying implementations of various sorting algorithms. Second, we evaluate its usability in verifying code developed for programming assignments of an undergraduate course. The first scenario represents usability by serious non-experts; the second represents usability on "standard code", developed without full functional verification in mind. We report our experiences and lessons learnt, from which we derive some general suggestions for furthering the development of verification tools with respect to improving their usability.
△ Less
Submitted 16 August, 2015;
originally announced August 2015.
-
Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model
Authors:
Alexander Heußner,
Christopher M. Poskitt,
Claudio Corrodi,
Benjamin Morandi
Abstract:
To harness the power of multi-core and distributed platforms, and to make the development of concurrent software more accessible to software engineers, different object-oriented concurrency models such as SCOOP have been proposed. Despite the practical importance of analysing SCOOP programs, there are currently no general verification approaches that operate directly on program code without additi…
▽ More
To harness the power of multi-core and distributed platforms, and to make the development of concurrent software more accessible to software engineers, different object-oriented concurrency models such as SCOOP have been proposed. Despite the practical importance of analysing SCOOP programs, there are currently no general verification approaches that operate directly on program code without additional annotations. One reason for this is the multitude of partially conflicting semantic formalisations for SCOOP (either in theory or by-implementation). Here, we propose a simple graph transformation system (GTS) based run-time semantics for SCOOP that grasps the most common features of all known semantics of the language. This run-time model is implemented in the state-of-the-art GTS tool GROOVE, which allows us to simulate, analyse, and verify a subset of SCOOP programs with respect to deadlocks and other behavioural properties. Besides proposing the first approach to verify SCOOP programs by automatic translation to GTS, we also highlight our experiences of applying GTS (and especially GROOVE) for specifying semantics in the form of a run-time model, which should be transferable to GTS models for other concurrent languages and libraries.
△ Less
Submitted 10 April, 2015;
originally announced April 2015.
-
Contract-Based General-Purpose GPU Programming
Authors:
Alexey Kolesnichenko,
Christopher M. Poskitt,
Sebastian Nanz,
Bertrand Meyer
Abstract:
Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU,…
▽ More
Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. The solution is integrated with the design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into the program text. We show that our library leads to modular and maintainable code that is accessible to GPGPU non-experts, while providing performance that is comparable with hand-written CUDA code. Furthermore, runtime contract checking turns out to be feasible, as the contracts can be executed on the GPU.
△ Less
Submitted 21 August, 2015; v1 submitted 24 October, 2014;
originally announced October 2014.
-
Verifying Monadic Second-Order Properties of Graph Programs
Authors:
Christopher M. Poskitt,
Detlef Plump
Abstract:
The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which are unable to express important global properties of graphs such as acyclicity, connectedness, or existence of paths.…
▽ More
The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which are unable to express important global properties of graphs such as acyclicity, connectedness, or existence of paths. In this paper, we extend the nested graph conditions of Habel, Pennemann, and Rensink to make them equivalently expressive to monadic second-order logic on graphs. We present a weakest liberal precondition construction for these assertions, and demonstrate its use in verifying non-local correctness specifications of graph programs in the sense of Habel et al.
△ Less
Submitted 16 June, 2014; v1 submitted 22 May, 2014;
originally announced May 2014.
