Hacking Internet Voting via Ballot Tampering

Dan Zimmerman and Joe Kiniry Election Day was this week.  If you took advantage of early voting, or you live overseas, you probably used a paper ballot you received in the mail a few weeks ago.  A digital alternative, being considered across the USA, is voting-by-email. To vote using email (Fig. 1), you download and […]

Read More

Innovation Week: Experiments, prototypes and new skills

During the first week of October, Galois held “Innovation Week,” a time for everybody to explore new ideas, recharge our creativity, have fun and share what we’ve learned and done with each other. Throughout the week, Galwegians worked on a diverse set of side projects: running experiments, building prototypes, solving puzzles and acquiring new skills.

Read More

Tech talk by Philip Wadler

abstract: We present four calculi for gradual typing: λB, based on the blame calculus of Wadler and Findler (2009); λC, based on the coercion calculus of Henglein (1994); and λT and λW, based on the three- some calculi with and without blame of Siek and Wadler (2010). We define translations from λB to λC, from […]

Read More

Tech Talk: Functional programming in Swift

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.) abstract: At this year’s WWDC, Apple announced Swift, a new programming language for iOS and OS X development. In this talk, I’d like to give a brief […]

Read More

2014 Bike Commute Challenge

Every September since 2007, Galois has participated in the annual Bike Commute Challenge. For the first time ever, Galois earned a top-ten finish among the 200-plus similarly sized companies that participated this year. This year’s 36.2% commute rate set a company record: Year Riders Trips Miles CommuteRate (%) Rank 2009 8 105 1115 15.2 50 […]

Read More

Why Xen?

Over the last few months, Galois has published or spoken about a variety of technologies based on the open source Xen hypervisor: our port of FreeRTOS on Xen, our MAC-enhanced version of the XenStore, and, of course, our continuing work on the Haskell Lightweight Virtual Machine (a.k.a., the HaLVM). Based on all this activity, I […]

Read More

Tech talk: Automatic Device Driver Synthesis

abstract: Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit, called Termite-2. Termite-2 is the first tool to combine the power of automation with the flexibility […]

Read More

Tech Talk: Verified Cryptographic Implementations

Abstract EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable security style and cryptographic implementations used in practice; as a consequence, real-world cryptography is sometimes considered as “one of the many ongoing disaster areas in security. We have […]

Read More