HCSS'22

file

Visible to the public Tiffin and MGen: An Expressive Policy Language with Multiple Runtime Monitoring Tools

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:

Abstract: Runtime monitoring for anomalous behavior of software systems is a critical validation technique as part of defense-in-depth cybersecurity solutions. Such techniques compliment static analyses and runtime pattern-matching based approaches that only identify known attacks and are thus likely to miss unknown or 0-day attacks.

file

Visible to the public Keynote Presentation: Thomas Dullien

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am
file

Visible to the public Machine Learning and the Unknown Unknowns

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:

Abstract: One of the important certification objectives for airborne software is demonstrating the absence of unintended behavior. In current software development processes, unintended behavior is associated with some identifiable structural feature, such as specific lines of code or a model element. However, in machine learning approaches to system development, unintended behavior may emerge from the data used to train the system.

file

Visible to the public Model-checking State Machines in the Wild

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:
Abstract: State machines are a compact representation of complex logical rules. State machines have diverse uses such as watchdog applications to monitor if a critical program has crashed, regular expression matching, and web services such as IFTTT (short for If This Then That) which has 18 million users running over 1 billion state machines. These state machines are often created for ad-hoc purposes with speed of development being a primary goal.
file

Visible to the public A Method for Formal Verification of Neural Network Collision Avoidance Controller

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

ABSTRACT

file

Visible to the public Correct-by-Learning Methods for Reliable Control

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

ABSTRACT: Computing systems that engage us physically with high degrees of autonomy pose longstanding challenges to formal methods. In particular, learning-based and data-driven approaches are quickly becoming indispensable in design, but their reliance on highly nonlinear function approximators and probabilistic reasoning has largely been at odds with the logical and symbolic analysis frameworks in formal methods.

file

Visible to the public Cyber Assured Systems Engineering at Scale

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

Abstract: Formal methods tools that provide mathematical proof of system properties have improved dramatically in their power and capabilities. As part of DARPA's Cyber Assured Systems Engineering (CASE) program, our team has developed a model-based systems engineering environment called BriefCASE that integrates formal methods at all levels of system design. Our methodology and tools enable systems engineers to address cybersecurity concerns early in the development of complex high-assurance systems.

file

Visible to the public Analyzing Code Stability Using Control Theoretic Techniques

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

You must register and request HCSS Community Membership to view the slides.

file

Visible to the public High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)

Submitted by Katie Dey on Wed, 04/27/2022 - 8:55am. Contributor:

Abstract: In the **High Assurance Rigorous Digital Engineering for Nuclear Safety** (HARDENS) project, Galois has developed a high-assurance, safety-critical demonstration system for the Nuclear Regulatory Commission using Rigorous Digital Engineering (RDE). The system in question is a Digital Instrumentation and Control (DI&C) system for Nuclear Power Plants (NPPs), and is called the Reactor Trip System (RTS).