HCSS 2023

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

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.