HCSS'22

file

Visible to the public Lowering the Barrier to Formal Modeling and Analysis

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
Abstract: Recent years have seen a significant increase in the application of formal methods to industrial systems. While this increase has been encouraging, there are still many tools which could provide practical, real-world benefits but that are impeded due to usability issues. These include packaging and installation issues, a lack of tooling integrated into traditional developer workflows, and limited visibility into automatedreasoning capabilities.
file

Visible to the public Automated Evidence Generation for Continuous Certification

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

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

file

Visible to the public Evolving Verified Cloud Authorization

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

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

file

Visible to the public Reasoning about Deltas — Even Doing Nothing is Difficult

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
Abstract: Formal software verification involves specifications, an implementation, and a proof that the implementation satisfies the specifications. When an actively-developed implementation evolves, the typical approach is to update the formal specifications and proof accordingly. The old version of specifications is simply relegated to history without attempting to formally relate the old and new versions.
file

Visible to the public P: Formal Modeling and Analysis of Distributed Systems

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

Abstract:

file

Visible to the public Keynote: What Log4j teaches us about the Software Supply Chain

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

Abstract
In December of 2021, exploit code for a high-severity zero-day vulnerability was released on GitHub. The exploit targeted a vulnerability in the default configuration of the widely-used log4j library and resulted in many open source and commercial codebases becoming instantly vulnerable. Attacks started immediately and vendors rushed to communicate their vulnerability status and remediation plans to customers.

file

Visible to the public CSAADE: Cryptographically Secure, Automatic Assurance Software Development Environment

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
The cyberattacks on the SolarWinds Orion products reinforce concerns about the vulnerability of the U.S. software supply chain and the insufficiency of current cybersecurity solutions in protecting all stages of the software development life cycle [1]. The Cryptographically Secure, Automatic Assurance Development Environment (CSAADE) mitigates the impact of software supply chain attacks by providing evidence-based evaluation of the software supply chain.
file

Visible to the public Lifting Formal Proof to Practice via an Assurance Case

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

Abstract: Formal Methods (FM) are important for verifying properties of systems with mathematical rigor. FM tools and techniques can provide a high level of confidence in a system (software, hardware, etc.), yet a mathematical proof is built on a mathematical model of a system. This gap between the model representation of the system and the operational use of the real-world system is particularly apparent in cyber-physical systems that interact with sensors and actuators, and require reasoning about environmental aspects, such as temperature and wind speed.

file

Visible to the public Model Validation for DARPA DPRIVE

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
Commodity hardware description languages (HDLs) like VHDL and Verilog present a challenge from a high assurance point of view because they lack formalized semantics: when a team of hardware engineers produce a circuit design in a commodity HDL and claims that it correctly implements a pseudocode algorithm, on what basis can that claim be evaluated?