HCSS Conference 2023

file

Visible to the public Keynote: From C to Rust: a Software Verification Journey

ABSTRACT

In recent years, formal verification has gone mainstream: both major open-source projects and large companies have embraced verified code for better safety, security and reliability.

file

Visible to the public Bridging the Gap between Protocol Specification and Program Verification

ABSTRACT

Implementing communication protocols correctly remains a huge challenge. Complex message formats and interdependencies paired with imprecise, incomplete or even contradictory English-language specifications make it hard to even define what "correct" means for a given protocol. The use of unsafe programming languages is of no help either and regularly leads to security vulnerabilities affecting millions of devices. At the same time, communication protocols are essential for today's connected world and often exposed to untrusted environments.

file

Visible to the public CRAM: C++ to Rust Assisted Migration

ABSTRACT

We present work performed at GrammaTech on semi-automated migration of legacy C++ code to Rust. A widely used systems programming language, C++ offers a historically rich set of language features, including low-level memory manipulation capabilities inherited from C. While such features can give rise to efficient programs, memory managed freely by the programmer often results in hard-to-debug program crashes and vulnerabilities.

file

Visible to the public Grading Open Source Software Development Practices

ABSTRACT

One of the most critical decisions a developer makes is the choice of which open source libraries to include in their application. Each library brings important functionality, but also imposes a maintenance burden. 85% of the vulnerabilities in open source software projects originate in the project's dependencies rather than the project code itself. As such, choosing libraries that prioritize security can make a substantial difference in the number of security issues a project has to deal with.

file

Visible to the public Signet-ring: A Framework for Authenticating Sources and Lineages of Digital Objects

ABSTRACT

Verifying sources of information is vital in assessing the credibility of facts and data in our increasingly digital world; often, the verification of the sources is as necessary as the information they provide. To battle misinformation and disinformation through digital objects, it is salient to provide consumers the ability to verify whether or not information (or data) provided by such sources was altered prior to its use (e.g., publication).

file

Visible to the public Leverageable Semantics Definitions and Contract Reasoning for a Technical Architecture Description Language

ABSTRACT

The Architecture and Analysis Definition Language (AADL) is an industry standard modeling language distinguished by its emphasis on strong semantics for modeling real-time embedded systems.

file

Visible to the public Oqarina – Mechanization of the AADL Architectural Description Language

ABSTRACT

The SAE AADL standard [1] provides the foundations for describing the architecture of safety-critical cyber-physical systems. AADL is a modeling language, equipped with a syntax definition and several legality and consistency rules that define the notions of model validity and its semantics. Several research activities illustrated how AADL can be used to model complex systems and to analyze them for key quality attributes such as performance, safety, or security.

file

Visible to the public Proteus: Automated Cyber Reasoning

ABSTRACT

In 2016, DARPA hosted the Cyber Grand Challenge (CGC), a competition to create automatic cyber reasoning systems. Together with a team from the University of Virginia, GrammaTech won second place out of over 100 teams. We present Proteus: the maturation of this technology from operating in a simple, controlled, and academic environment to modern, real-world operating systems.

file

Visible to the public Semantic Backplane for Model-Based Development

ABSTRACT

A well-known challenge of end-to-end tooling of CPS products in the aerospace and automotive industries is heterogeneity and the large number of distinct tools required in the model-based engineering process. Composition and verification of heterogeneous, interacting product models requires an end-to-end integrated tool chain that includes a diverse collection of COTS, open source, and proprietary tools. This is difficult because it is not simply a tool interoperability problem, but rather a major semantic integration problem.

file

Visible to the public MAESTRO: Measurement and Attestation Execution and Synthesis Toolkit for Remote Orchestration

ABSTRACT

The ultimate goal of a sound attestation process is to establish the integrity of a target of measurement - one or more components on a target system whose integrity is of interest to the consumer of an attestation. Copland is a domain- speci c-language for specifying remote attestation protocols with primitives for layered measurement, remote requests, and cryptographic evidence bundling.