Cybersecurity and Software Assurance
Permanent URI for this collection
Browse
Recent Submissions
1 - 5 of 5
-
ItemMatching Possible Mitigations to Cyber Threats: A Document-Driven Decision Support Systems Approach( 2020-01-07)Despite more than a decade of heightened focus on cybersecurity, the threat continues. To address possible impacts, cyber threats must be addressed. Mitigation catalogs exist in practice today, but these do not map mitigations to the specific threats they counter. Currently, mitigations are manually selected by cybersecurity experts (CSE) who are in short supply. To reduce labor and improve repeatability, an automated approach is needed for matching mitigations to cyber threats. This research explores the application of supervised machine learning and text retrieval techniques to automate matching of relevant mitigations to cyber threats where both are expressed as text, resulting in a novel method that combines two techniques: support vector machine classification and latent semantic analysis. In five test cases, the approach demonstrates high recall for known relevant mitigation documents, bolstering confidence that potentially relevant mitigations will not be overlooked. It automatically excludes 97% of non-relevant mitigations, greatly reducing the CSE’s workload over purely manual matching.
-
ItemSynthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel( 2020-01-07)We describe a method and tools for the creation of formally verified components that run on the verified seL4 microkernel. This synthesis and verification environment provides a basis to create safe and secure critical systems. The mathematically proved space and time separation properties of seL4 are particularly well-suited for the miniaturised electronics of smaller, lower-cost Unmanned Aerial Vehicles (UAVs), as multiple, independent UAV applications can be hosted on a single CPU with high assurance. We illustrate our method and tools with an example that implements security-improving transformations on system architectures captured in the Architecture Analysis and Design Language (AADL). We show how input validation filter components can be synthesized from regular expressions, and verified to meet arithmetic constraints extracted from the AADL model. Such filters comprise efficient guards on messages to/from the autonomous system. The correctness proofs for filters are automatically lifted to proofs of the corresponding properties on the lazy streams that model the communications of the generated seL4 threads. Finally, we guarantee that the intent of the autonomy application logic is accurately reflected in the application binary code hosted on seL4 through the use of the verified CakeML compiler.
-
ItemMeasuring Confidence of Assurance Cases in Safety-Critical Domains( 2020-01-07)Evaluation of assurance cases typically requires certifiers’ domain knowledge and experience, and, as such, most software certification has been conducted manually. Given the advancement in uncertainty theories and software traceability, we envision that these technologies can synergistically be combined and leveraged to offer some degree of automation to improve the certifiers’ capability to perform software certification. To this end, we present DS4AC, a novel confidence calculation framework that 1) applies the Dempster-Shafer theory to calculate the confidence between a parent claim and its children claims; and 2) uses the vector space model to evaluate the confidence for the evidence items using traceability information. We illustrate our approach on two different applications, where safety is the key property of interest for both systems. In both cases, we use the Goal Structuring Notation to represent the respective assurance cases and provide proof of concept results that demonstrate the DS4AC framework can automate portions of the evaluation of assurance cases, thereby reducing the burden of manual certification process.
-
ItemProtecting Temporal Fingerprints with Synchronized Chaotic Circuits( 2020-01-07)In recent years, connected autonomous vehicles (CAVs) feature an increasing number of Ethernet-enabled electronic control units (ECUs), thereby creating more threat vectors that provide access to the Controller Area Network (CAN) Bus. Currently, mitigation techniques to protect the CAN bus from compromised ECU units in vehicle ad hoc networks (VANET) often utilize classical cryptographic techniques. However, ECUs often have temporal signatures that leak internal state information to eavesdropping attackers who can leverage temporal properties for longitudinal attacks. Unfortunately, these types of attacks are difficult to defend against using classical encryption schemes and intrusion detection systems (IDS) due to their high computational demands and ineffectiveness at protecting CAVs throughout the duration of their long lifespans. In order to address these problems, we propose a novel cryptographic framework that protects information embedded in ECU network communications by delivering an encryption system that periodically "salts" the temporal dynamics of individual ECU units with chaotic signals that are difficult to learn. We demonstrate the framework on two datasets, and our results show that the underlying temporal signatures cannot be approximated by state-of-the-art learning algorithms over finite time horizons.
-
Item