Presentation

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].

file

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

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

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

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

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

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

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

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

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

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

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

Submitted by John Hatcliff on Wed, 03/29/2023 - 11:25am. Contributor:

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

Submitted by jhugues on Wed, 03/29/2023 - 11:25am. Contributor:

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

Submitted by bbierman on Wed, 03/29/2023 - 11:25am. Contributor:

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

Submitted by danielbala on Wed, 03/29/2023 - 11:25am. Contributor:

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.