Galois

file

Visible to the public Proving Amazon's s2n Correct

Submitted by Katie Dey on Tue, 04/11/2017 - 5:36pm. Contributor:

Presented as part of the 2017 HCSS conference.

ABSTRACT

file

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

Submitted by brad_martin on Sat, 04/26/2014 - 7:08am. Contributor:

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

Submitted by leepike on Wed, 04/23/2014 - 5:39am. Contributor:

Presented as part of the 2014 HCSS conference.

Abstract:

file

Visible to the public TrackOS: a Security-Aware RTOS

Submitted by TimTh on Tue, 05/14/2013 - 12:33pm. Contributors:

Presented as part of the 2013 HCSS conference.

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

Submitted by TimTh on Mon, 05/13/2013 - 4:00pm. Contributor:

Presented as part of the 2013 HCSS conference.

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.