Galois

file

Visible to the public Proving Amazon's s2n Correct

ABSTRACT

file

Visible to the public High Assurance Cryptography Synthesis with Cryptol

Abstract:

HCSS participants, in the main, know about Galois' Cryptol language and system and its capabilities. In short, Cryptol is a domain-specific language for programming, executing, testing, and formally reasoning about streams of bits. Cryptol particularly excels at specifying and reasoning about cryptographic algorithms. As summarized last year at HCSS, Galois has "rebooted" Cryptol and created, from the ground up, a new Open Source Cryptol release: Cryptol version 2.

file

Visible to the public Cryptol version 2: An Open Source Cryptol

Abstract

HCSS participants, in the main, know about Galois' Cryptol language and system and its capabilities. In short, Cryptol is a domain-specific language for programming, executing, testing, and formally reasoning about streams of bits. Cryptol particularly excels at specifying and reasoning about cryptographic algorithms.

Galois has decided to "reboot" Cryptol and create, from the ground up, a new Open Source Cryptol release: Cryptol version 2.

file

Visible to the public Programming Languages for High-Assurance Autonomous Vehicles

Abstract:

I will discuss how, in just 1.5 years, Galois built two new domain-specific languages (DSLs) and used them to develop a "hack-proof", full-featured unpiloted air system. The secret to our increased productivity and assurance was building embedded DSLs, in which the DSLs are libraries in Haskell. We generate embedded C code that is guaranteed to be memory-safe from a relatively small specification.

The autopilot and more information is available at smaccmpilot.org.

Speaker Bio:

file

Visible to the public Multi-App Security Analysis: Looking for Android App Collusion

Abstract:

The Android security model was built from the ground up to combat potential attacks (or misuse) one app at a time. This model culminates in a user interface that asks for the user's approval each time an app is installed. While the interfaces enables users to avoid applications that may violate their security policy (by using combinations of permissions) applications can freely communicate with each other to share their permissions, achieving capabilities through collusion that astute users would not have approved.

file

Visible to the public TrackOS: a Security-Aware RTOS

ABSTRACT

Cyber-physical systems (CPS) are becoming an increasingly attractive target for adversaries to launch software attacks against. New approaches are needed to detect software-based vulnerabilities while meeting the constraints of embedded execution in CPS.

file

Visible to the public Techniques for Scalable Symbolic Simulation

ABSTRACT

Symbolic simulation is a powerful technique for building mathematical models describing a program's results by simulating execution while interpreting inputs as symbolic variables. Such models can then be used to prove properties about the corresponding source program, including equivalence against a reference implementation.

file

Visible to the public FUSE: Inter-Application Security for Android

Abstract:

The Android platform currently provides only limited support for preventing collusion between multiple apps installed on the same device: the main security mechanism is that at installation time each individual app is required to declare a manifest of the Android permissions it needs to operate.

file

Visible to the public Verification of Elliptic Curve Cryptography

Abstract:

Cryptography is essential for ensuring that sensitive information can be securely stored and transmitted without risk of tampering or disclosure to untrusted parties. Although typically only a very small part of an overall system, cryptographic implementations are often highly complex due to a variety of performance optimizations, and may have many edge cases or diffcult to understand implementation tricks.