Galois and voidALPHA Produce Free Game for DARPA to Help Crowdsource Software Security

As part of DARPA’s Crowd Sourced Formal Verification (CSFV) program, Galois has partnered with game design and development experts voidALPHA to produce a free online formal verification game, StormBound.

Formal verification is the most rigorous way to thwart attacks against IT systems and applications upon which military, government, and commercial organizations rely. Traditional formal methods, however, require specially trained engineers to manually scour software—a process that up to now has been too slow and costly to apply beyond small software components. In contrast, CSFV games such as StormBound translate players’ actions into program annotations and generate mathematical proofs to help verify the absence of important classes of flaws in software written in the C programming language. We have developed an automated process that creates new puzzles for each verification problem in need of a solution. With StormBound, we aim to investigate whether large numbers of non-experts playing the game can perform formal verification faster and more cost-effectively than conventional processes.

For more information, contact Aaron Tomb or Jef Bell.

Approved for Public Release, Distribution Unlimited


Galois IPv6 Rollout

One of our IT goals for 2014 is enabling IPv6 on all our current IPv4 subnets. I was pleased to see Shumon Huque's full-day IPv6 tutorial on the LISA '13 schedule. I hoped he could fill the gaps in my limited experience with IPv6 and provide me the knowledge I'd need to configure our network hardware and applications.

Full-day technical tutorials can sometimes test my patience, but Shumon's presentation moved quickly while remaining clear. I came away from the day thinking that I had enough basic knowledge to plan and implement our IPv6 rollout.

Returning to Portland, I had to upgrade a couple core switches and apply to our ISP for a netblock prior to enabling it on our network, but once the hardware was in place, everything went reasonably well.

Shumon's overview had done exactly what I'd hoped it would: allow me to interpret the various bits of vendor-specific and application-specific documentation and assemble a reasonable roll-out plan.

Our DMZ and client networks are now fully IPv6 enabled. (Internal development networks will take a bit more time due to some additional complexity.)

Along the way, I learned a couple things Shumon didn't explicitly cover in his presentation.

  1. Make sure that reverse DNS pointers are in place for any mail server before enabling IPv6. gmail (among others) will reject messages from any mail server without reverse DNS pointers in place.
  2. The ip6tables that ships with RHEL/CentOS 5 has a limited ability to do stateful packet inspection. The generic rule allowing packets from established or related sessions does not work:
       # this is broken in RHEL/CentOS 5
       -A INPUT -m state --state ESTABLISHED,RELATED -j ACCEPT
  3. Third, it was a lot of fun! Nearly all our DMZ services (NTP, DNS, Jabber, e-mail, www, ssh, host-based firewalls) needed updated configurations, so I learned a bunch. The day after I did the initial rollout, one of our engineers came into the office, turned off IPv4 on his Mac, and tested what percentage of Google result links he could follow. (He thought about 5%, though he said the queries he chose probably resulted in a higher success rate than might be normal.)
  4. Finally, I've been mildly surprised at the quantity of IPv6 packets traversing our border firewall. Over the past week, IPv6 has comprised 38% of overall inbound traffic and 11% of outbound. The numbers are similar when scoped to the past month.

I'd like to express my thanks to Shumon for the talk and the LISA organizers for putting it on the schedule!


Portland Linux/Unix Group Advanced Topics: Android App Collusion

Rogan Creswick will be giving the next Portland Linux/Unix Group's (PLUG) Advanced Topics presentation, "Multi-App Security Analysis: Looking for Android App Collusion." The event, hosted by PLUG, will be held next Tuesday, Nov. 19th at 7:00 p.m. at Free Geek, 1731 SE 10th Avenue, Portland, OR (map).


The Android permission model opens up a number of opportunities for apps to bypass the established single-app permission checks that Android users rely on to control data flow and application behavior on their devices. I'll do my best to terrify the Android-using audience by describing the attack surface for colluding applications and showing interactive visualizations of multi-app data flow. We'll look at the Android permission model, the user-interface it results in, and I'll show just how easy it is to make apps that look innocuous.


Rogan Creswick develops unique tools and techniques for software development and security analysis at Galois, Inc. His research interests focus on improving the state of the art in software engineering tools and user interfaces. His experience also reaches into the areas of user interface automation and customization via integrated assistants and automated documentation aides at IBM Research. He has striven to provide natural interfaces to ease communication with complex and semi-sentient agents through existing tools that have already become trustworthy and familiar to their users.


Rob Wiltbank Joins Galois, Inc. as CEO

Portland, Oregon (October 30, 2013) - Rob Wiltbank, Ph.D. has joined Galois as its CEO. Rob is widely recognized as a world expert in angel investing performance and entrepreneurial strategy. In his new role, Rob will drive strategy for Galois' growth, oversee business operations and development, and help commercialize its technologies.

"I'm tremendously pleased to welcome Rob aboard," said John Launchbury, Galois' Chief Scientist and founder. "His extraordinary business insights and energetic leadership combine wonderfully with the technical strength of our team. Watch this space, because great things will ensue!"

Prior to Galois, Rob was a professor at Willamette University's Atkinson Graduate School of Management, ranked by Inc. Magazine as a "top 10" in entrepreneurship education, where he ran the Willamette Angel Fund and entrepreneurship courses. Over the years, Rob’s research has focused on strategy-making under uncertainty and entrepreneurial expertise, particularly as it relates to growing new organizations.

He received the prestigious 2013 Hans Severiens Award, honoring individuals whose actions demonstrate leadership in advancing the role of angel investing in expanding entrepreneurship and the angel investment industry as a whole. He is on the board of the Angel Resource Institute and serves on the Editorial Board of the Journal of Business Venturing. Additionally, Rob was a partner with Montlake Capital, a growth equity fund, and a Co-Founder of Revenue Capital Management, an innovative revenue capital fund. 

Rob is co-author of the 2009 book The Catalyst: How You Can Become an Extraordinary Growth Leader selected by Business Week as one of the best books on innovation and design in 2009. He is also co-author of Effectual Entrepreneurship, a text based on 15 years of academic research into entrepreneurial expertise. Rob earned his Ph.D. in Strategy from the University of Washington, and a degree in Finance and Accounting from Oregon State University.



Tech Talk: Programming Diversity

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: Programming Diversity
speaker: Ashe Dryden
time: Tuesday, 22 October 2013, 10:30am
location: Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: It's been scientifically proven that more diverse communities and workplaces create better products and the solutions to difficult problems are more complete and diverse themselves. Companies are struggling to find adequate talent. So why do we see so few women, people of color, and LGBTQ people at our events and on the about pages of our websites? Even more curiously, why do 60% of women leave the tech industry within 10 years? Why are fewer women choosing to pursue computer science and related degrees than ever before? Why have stories of active discouragement, dismissal, harassment, or worse become regular news?

In this talk we’ll examine the causes behind the lack of diversity in our communities, events, and workplaces. We’ll discuss what we can do as community members, event organizers, and co-workers to not only combat this problem, but to encourage positive change by contributing to an atmosphere of inclusivity.

bio: Ashe Dryden is an indie ruby developer living in Madison, WI. She's been involved with the web in some form or another over the course of the past 12 years. Ashe is an outspoken educator for diversity, inclusiveness, and empathy. She's currently writing a book on increasing diversity within companies, as well as working on a video series and site to serve as a resource to people who want to get involved. When she isn't discussing technology or it’s intersection with culture, she's cycling, tweeting, playing board games, debating the social implications of Star Trek episodes, being that awkward girl at the party, and waiting for her next burrito fix.