HCSS Conference 2023

file

Visible to the public Scalable and Provable Distributed SAT Solving

Submitted by Anonymous on Wed, 03/29/2023 - 11:26am. Contributors:

Abstract

SAT and SMT solvers are the "engines of proof" that underly many of our automated reasoning tools. At Amazon, we make billions of calls to SAT and SMT solvers each day. Recent progress in distributed SAT solving has led to solvers that can solve problems 30-50 times faster on average (up to one hundred times faster) than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem.

file

Visible to the public Synergizing Model-based and Data-driven Methods for CPS Design

Submitted by Sandeep Neema on Wed, 03/29/2023 - 11:26am. Contributor:

Abstract

Model-based engineering approaches are now recognized as integral to design and operation of commercial as well as military Cyber Physical Systems. The fundamental premise of model-based engineering is semantically precise representations of a system at high-levels of abstraction that can be rigorously analyzed and systematically refined into build and implementations, leading towards a correct-by-construction design.

file

Visible to the public A Unified View of Weirdness: A Logical Framework for Emergent Execution

Submitted by William Harrison on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

For any software application, there are multiple worlds relevant to modeling emergent execution (see inset figure). The design-level world re ects programmer intentions and language abstractions, the binary world reflects the concrete representations of these abstractions, and the platform world reflects the ground truth of this application in operation.

file

Visible to the public Cheesecloth: Zero-Knowledge Proofs of Real-World Vulnerabilities

Submitted by Anonymous on Wed, 03/29/2023 - 11:26am. Contributors:

ABSTRACT

Currently, when a security analyst discovers a vulnerability in critical software system, they must navigate a dilemma: immediately disclosing the vulnerability to the public could harm the system's users; whereas disclosing the vulnerability only to the software's vendor lets the vendor disregard or deprioritize the security risk, to the detriment of unwittingly-affected users.

file

Visible to the public Incorrectness Logic for Scalable Bug Detection

Submitted by Anonymous on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

Incorrectness Logic (IL) has recently been advanced as a logical under-approximate theory for proving the presence of bugs--dual to Hoare Logic, which is an over-approximate theory for proving the absence of bugs. To facilitate scalable bug detection, later we developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic and its frame rule.

file

Visible to the public Keynote: Underapproximate Reasoning at Scale

Submitted by Anonymous on Wed, 03/29/2023 - 11:26am. Contributor:

Abstract

I recount lessons learned from a decade of experience in industry on logical methods for reasoning about programs at scale. It started with the shock of bumping program reasoning, usually a "move slow and break nothing" approach, up against fast-paced industrial software development practices. Gradually, I came to appreciate the importance of proving the presence of bugs as well as the much rarer case of proving their absence, and together with many colleagues I sought foundations for and applications of under-approximate reasoning at scale.

file

Visible to the public Zappa for Correctly Implementing CPSA Analyzed Protocols

Submitted by ramsdell on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

The Cryptographic Protocol Shapes Analyzer CPSA determines if a cryptographic protocol achieves authentication and secrecy goals. It can be difficult to ensure that an implementation of a protocol matches up with what CPSA analyzed, and therefore be sure the implementation achieves the security goals determined by CPSA.

file

Visible to the public Reasoning about the Robustness of Protocols

Submitted by Eunsuk Kang on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

A typical protocol makes various assumptions about the environment in which it is deployed. For instance, to guarantee a security requirement, a protocol may rely on the attacker not having prior knowledge of secrets that the system relies on, or the end user correctly carrying out a key protocol step (e.g., browser authentication). Similarly, a distributed protocol typically relies on assumptions about the reliability of the underlying network (e.g., a message is delivered without corruption; certain network nodes are always connected).

file

Visible to the public Secure Device Design via Protocol Analysis

Submitted by guttman on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

Protocol analysis tools such as cpsa and Tamarin are designed to explore all of the behaviors possible for a protocol that uses cryptography when it interacts with an adversary as well as other compliant peers. However, the word protocol may be understood in a wide sense. Since both of those analysis tools allow modeling mutable state as well as message passing, they can be used to model, analyze, and redesign security-relevant devices.

file

Visible to the public Formal Verification of Security and Privacy Requirements in Modern ICT Systems Assisted by the Tamarin Security-protocol Prover

Submitted by Anonymous on Wed, 03/29/2023 - 11:26am. Contributor:

ABSTRACT

Over the last 3-5 years, we developed several formal-methods theories in order to be able to verify specific aspects of security and privacy in different modern and protocols. These theories were then implemented entirely or via some approximation in formal specifications in the Tamarin prover [6].