Viewing Results for "cryptol" (5 of 6 Pages)

Part one: Verifying s2n HMAC with SAW

In June 2015, Amazon introduced its s2n library, an open-source TLS library that prioritizes simplicity. A stated benefit of this simplicity is ease of auditing and testing. Galois recently collaborated with Amazon to show that this benefit extends to verifiability by proving the correctness of s2n’s implementation of the keyed-Hash Message Authentication Code (HMAC) algorithm. To construct this […]

Read More

Galois Announces ISC: The Imperfect Stitch Compiler

This was an April Fool’s post published on April 1, 2016. The Imperfect Stitch Compiler is a fictional product. Galois is known for building perfect software. But is our software too perfect? The imperfect stitch, or Persian flaw, is a deliberate error in an otherwise perfect work of art. The term derives from the proverb, […]

Read More

Galois: 2015 highlights

2015 was an active and productive year at Galois. From numerous awards, to new projects and spin-offs, to a vast array of publications and talks, Galwegians contributed to a wide range of fields this year. In this post, we highlight some of the contributions we made in 2015.

Read More

Tech talk: A Brief History of Verifiable Elections

abstract: Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that […]

Read More

Announcing the Software Analysis Workbench

We are pleased to announce a public preview of the Software Analysis Workbench. The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW […]

Read More

Block Ciphers, Homomorphically

by Brent Carmer and David W. Archer, PhD Our team at Galois, Inc. is interested in making secure computation practical. Much of our secure computation work has focused on linear secret sharing (LSS, a form of multi-party computation) and the platform we’ve built on that technology. However, we’ve also done a fair bit of comparison […]

Read More

Tech Talk: A Gentle Introduction to Hiding Usage Patterns

Galois is pleased to host the following tech talk. These talks are open to the interested public–please join us! (There is no need to pre-register for the talk.) title: A Gentle Introduction to Hiding Usage Patterns speaker: Rafail Ostrovsky time: Friday, 25 April 2014, 10am location: Galois Inc. 421 SW 6th Ave. Suite 300, Portland, […]

Read More

Heartbleed: A great time to think about incident response

Heartbleed is the nickname of a dangerous OpenSSL vulnerability that was just announced. A security update was already available before the announcement, and this is definitely a vulnerability where quickly patching makes a big difference. A fast response matters here because malware wasn’t in the wild yet, so many sites likely can prevent any negative consequences […]

Read More

High-Assurance Base64

Author: David Lazar Galois’ mission is improving the trustworthiness of critical systems. Trustworthiness is an inherent property of a system, but we need to produce evidence of its trustworthiness in order for people to make informed decisions. The evidence, and its presentation is a key part of what is often called an assurance case. The […]

Read More