HCSS'14

file

Visible to the public Keynote Presentation: Neal Ziring

Submitted by brad_martin on Mon, 04/28/2014 - 11:14am. Contributor:

Presented as part of the 2014 HCSS conference.

Abstract

file

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

Submitted by brad_martin on Sat, 04/26/2014 - 8: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 Using Coq to Verify DPLL

Submitted by kendroe on Sat, 04/26/2014 - 7:29am. Contributor:

Abstract

Most large software systems have complex data structures with complex invariants. Many bugs can be traced to code that does not maintain these invariants. As an example, the Heartbleed bug can be traced to an attacker sending a packet that violates an invariant that is assumed to be true in the OpenSSL code. Often these invariants are not well documented. However, maintaining them is necessary for correct operation of the software.