HCSS '22

file

Visible to the public Keynote Presentation: A Navy of Things: The Role of IoT at War

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

Roger A. Hallman is a cybersecurity researcher with the Naval Information Warfare Center (NIWC) Pacific in San Diego, California. He is also a PhD Candidate under the supervision of Professor George Cybenko at Dartmouth College in Hanover, New Hampshire. His previous research efforts spanned applied homomorphic encryption, resilient cloud-based services, malware analysis, and decision support for cybersecurity.

file

Visible to the public Kani Rust Verifier

Submitted by Katie Dey on Wed, 04/27/2022 - 8:57am. Contributors:
Abstract: Rust has made significant inroads as a popular safe systems programming language over the decade since its release.  Stack Overflow has named Rust the "most loved language" every year since  2016.  One of the language's main selling points is its focus on reliability---the ownership type system is a success story of programming language memory safety research breaking into the mainstream.
file

Visible to the public Fiat Cryptography: A Formally Verified Compiler for Finite-Field Arithmetic

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

Abstract: Fiat Cryptography is a formally verified compiler for cryptographic arithmetic code, bridging the gap between whiteboard-level math and performant C code. It started as an MIT project developed mostly by undergrads and has since been adopted by very popular open-source projects, including Chrome and Firefox. I will give background on the problem and solution, the latter being a split between coding and proving generic algorithms as functional programs, using partial evaluation to specialize those programs to parameters, and then applying relatively tra

file

Visible to the public Using Lightweight Formal Methods to Validate a Key-value Storage Node in Amazon S3

Submitted by Katie Dey on Wed, 04/27/2022 - 8:57am. Contributor:
Abstract: This talk reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By “lightweight formal methods” we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team.
file

Visible to the public Demystify Your Trust Boundary With Interactive Refinement

Submitted by Katie Dey on Wed, 04/27/2022 - 8:57am. Contributor:
Automated reasoning can precisely answer questions about system behavior, but traditionally requires a huge up-front investment. The traditional approach begins with asking the user to provide a complete formal specification, which can be expensive in time and effort. It then checks if the implementation matches the specification, providing value to its user at the end of this process.
file

Visible to the public Formally Verifying Security and Compliance Mandates using AWS Network Access Analyzer

Submitted by Katie Dey on Wed, 04/27/2022 - 8:57am. Contributor:
Abstract: Amazon Web Services (AWS) Customers use the Virtual Private Cloud service to virtually provision networks to connect their cloud-based applications. As customer’s scale their networks in order to meet their business goals it becomes more and more challenging to determine if their applications continue to meet their security and compliance mandates.
file

Visible to the public Unified Configuration Modeling Infrastructure

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

Abstract: Modern software systems, ranging from home networks to nation-critical infrastructures, are assembled from general COTS and open-source components. These components are built to be versatile - usable in a variety of different contexts. For a system to accomplish its mission, its components must be properly configured to interoperate. However, system configuration is complicated in practice: local configuration changes often have a profound system-wide effect. Misconfiguration can both hamper system functionality and have severe security repercussions.

file

Visible to the public Keynote Presentation: Supply Chain Events: Hardware vs. Software

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

Visible to the public Scaling Formal Verification with Specification Extraction

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
Abstract: Formal verification is a powerful tool for assuring software systems. By building machine-checked mathematical proofs that software meets its specifications, formal verification provides high confidence that softwareis correct and free of vulnerabilities. Unfortunately, formal verification is also difficult and expensive, specifically for programs that use and manipulate pointers.
file

Visible to the public Proof, but at What Cost?

Submitted by Katie Dey on Wed, 04/27/2022 - 8:56am. Contributor:
Abstract: Dafny is a verification-aware programming language that aims to make formal verification more accessible to programmers and students. The Dafny toolchain includes a verifier that translates Dafny programs to Boogie, an intermediate verification language that supports verifying specifications by invoking an SMT solver such as Z3.