HCSS 2023

file

Visible to the public Raad.pdf

Submitted by akarns on Mon, 04/24/2023 - 8:40am
file

Visible to the public Zelkova - 100 Million+ SMT Queries a Day

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

ABSTRACT

Zelkova is a distributed system that uses automated reasoning to answers logical questions about security policies, like "does principal A have access to resource B" or "is resource C accessible by unauthenticated principals." Zelkova does this by translating both the input policy and question into an SMT query and calling a portfolio of solvers. Launched five years ago, Zelkova has become a critical part of Amazon Web Services (AWS) "provable security" initiative, growing to process over a billion SMT queries a day.

file

Visible to the public Capabilities Labeling

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

Abstract

The goal of reverse engineering (RE) is to determine the purpose and intent of software, such as legacy binaries, malware, or COTS components of unknown provenance. While RE tools have improved, the task is still daunting, especially for stripped binaries with no function or variable names. Understanding such code is a time-consuming, attention-demanding, and error-prone task, and the skills applied by experts can take years of experience to develop. Many state-of-the-art RE tools provide primarily generic information, such as entry-points or reachability.

file

Visible to the public Verification-Guided Development of the Cedar Authorization Language

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

ABSTRACT

Cedar is an authorization policy language used to express permissions for an application and authorize users' actions accordingly. An authorization policy governs which principal in a system can perform what actions on a given resource. For example, a policy for a photo-sharing application might state that the application's users can delete only the photos they own. The application backend enforces this policy by invoking the authorization engine to check if a delete request is allowed.

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.