HCSS'14: Poster Session

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.

file

Visible to the public Toward Precise and Accurate Descriptions of Weaknesses

Submitted by Paul E. Black on Fri, 04/25/2014 - 10:20am. Contributor:

Abstract:

MITRE's Common Weakness Enumeration (CWE) http://cwe.mitre.org/ is a list of several hundred classes of weakness that may be found in software. While it is a huge amount of progress over what was available a decade ago, there is still a lot of work to do. We propose some directions to significantly improve CWEs. These directions come from semantic templates, software fault patterns, and other work.