HCSS Conference 2023

file

Visible to the public Assurance-Case Driven Framework to Support Cyber-Physical Systems

ABSTRACT

The safety and security of cyber physical systems (CPS) play an important role many safety-critical sectors. The software assurances to cyber physical systems depend on the correctness, resilience and integrity that can be achieved not only before the deployment time but also the run-time. However, there some serious challenges when developing safe and secure cyber physical systems. In this talk, we introduce a novel assurance case driven framework that emphasizes on the following two perspectives.

file

Visible to the public Model-based Reasoning Tool for Software Ecosystems

ABSTRACT

Over the past decades, software domains have witnessed a trend towards faster software release cycles, an increase of software components, and their connectivity. Examples include cyberphysical system in Industry 4.0 domains such as health care, retail, or transportation, in which, technically, software components are connected to a software ecosystem. Faster release cycles and high connectivity make many software ecosystem updates an expensive, arduous, and risky maintenance task.

file

Visible to the public Scalable Industrial Control System Fuzzing Using Explainable AI

ABSTRACT

Learning-based modeling and fuzzing of industrial control systems (ICS) has shown promising results to find ICS attacks without requiring domain-specific expertise. However, ICS fuzzing faces the key challenge of state explosion, where the fuzzing space grows exponentially with ICS size. In this paper, we propose to exploit explainable AI (XAI) to address this challenge. Our results show that XAI accurately explains the ICS model and significantly speeds-up attack fuzzing by 64x.

BIO

file

Visible to the public Bindle: Automatic Harness Generation

ABSTRACT

file

Visible to the public Lifecycle Attestation

ABSTRACT

file

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

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

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

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.