HCSS'19 Poster Session

file

Visible to the public Reasoning with Assurance Arguments under Uncertainty – Composing Formal and Non-Formal

Submitted by akarns on Thu, 05/09/2019 - 1:50pm. Contributors:

A significant challenge in automating certification of software intensive complex computing systems is information heterogeneity that runs the gamut from non-formal artifacts such as safety analyses, operational guidance, unit tests, and simulation runs to, more recently, formal artifacts. An emerging approach to certification of such software systems is the use of assurance cases to provide goal-based arguments supported by evidence.

file

Visible to the public Affix: Binary Model Generation for Static Analysis

Submitted by mwhicks1 on Wed, 05/08/2019 - 3:20pm. Contributor:

Static analysis and dynamic analysis are the yin and yang of program analysis. Static analysis has the benefit that it can reason about many, or all, runs of a program at once. However, to do that it must abstract aspects of the programs semantics. For large or complicated programs, the resulting imprecision can lead to an intolerable number of false-positive alarms. Dynamic analysis reasons about particular program executions precisely, using a (perhaps automatically generated) test suite.

file

Visible to the public ACE Assurance, Composed, and Explained

Submitted by pranavsrinivas on Wed, 05/08/2019 - 2:42pm. Contributors:

The state-of-the-art in systems assurance is based on testing, simulation and certification, and it is currently incorporating formal verification for some of the system's components. Formal verification has a limited use at present because it calls for a clean slate design and development, which are not always possible or practical, and because it is computationally challenging for large systems. Therefore, formal verification is commonly constrained to single software or hardware components that can be adequately modeled.

file

Visible to the public Integrated Data Space Randomization and Control Reconfiguration for Securing Cyber-Physical Systems

Submitted by Bradley Potteiger on Wed, 05/08/2019 - 2:42pm. Contributors:

Cyber-Physical Systems (CPS) have been increasingly subject to cyber-attacks including code Non-control data attacks have become widely popular for circumventing authentication mechanisms in websites, servers, and personal computers. Moreover, in the context of Cyber-Physical Systems (CPS) attacks can be executed against not only authentication but also safety. With the tightly coupled nature between the cyber components and physical dynamics, any unauthorized change to safety-critical variables may cause damage or even catastrophic consequences.

file

Visible to the public Information Exposure (IEX) Class in the Bugs Framework (BF)

Submitted by akarns on Wed, 05/08/2019 - 2:42pm. Contributors:

Exposure of sensitive information can be harmful on its own and in addition could enable further attacks. A rigorous and unambiguous definition of information exposure faults can help researchers and practitioners identify them, thus avoiding security failures. This poster describes Information Exposure (IEX), a new class in the Bugs Framework (BF). BF comprises rigorous definitions and (static) attributes of fault classes, along with their related dynamic properties, such as proximate and secondary causes, consequences and sites.

file

Visible to the public Practical Application of SPARK to OpenUxAS: Initial Results

Submitted by Anonymous on Wed, 05/08/2019 - 2:42pm. Contributors:

Formal methods provide powerful tools for the analysis of complex software, enabling engineers to establish assurance of high quality in their software. The SPARK language and tools build upon the foundation of Ada and allow engineers to program not only their software, but also their specifications and their proofs. SPARK thus provides engineers a practical, industrial strength formal method.