Solving Sudoku Using Cryptol

Cryptol is a language tailored for cryptographic algorithms. Sudoku is a popular puzzle the reader  is no-doubt already familiar with. We will offer no deep reason why anyone should try to solve Sudoku in Cryptol; other than the very fact that it'd be a shame if we couldn't!Needless to say, Cryptol has not been designed for encoding search algorithms. Nonetheless, some of the features of Cryptol and its associated toolset make it extremely suitable for expressing certain constraint satisfaction problems very concisely; and Sudoku very nicely falls into this category.

Representing the board

A Sudoku board can be represented in a variety of ways. We will pick the simplest: A sequence of 9 rows, each of which has 9 elements storing the digits. Each digit will require 4 bits; since they range from 1 to 9. So, a good Cryptol type for a board is:

  [9][9][4]

In Cryptol-speak, this type simply represents a sequence of precisely 9 elements, each of which is a sequence of 9 elements themselves, each of which are 4-bit words. (Technically, the type [4] also represents a sequence of precisely 4 elements, each of which are bits. But it's easier to read that as 4-bit words. The type [4] and [4]Bit are synonymous in Cryptol, and can be used interchangeably in all contexts.)

Click to read more ...

Tech Talk: Fun with Dependent Types

The March 24th Galois Tech Talk was delivered by Aaron Tomb, titled "Fun with Dependent Types."

• Date: Tuesday, March 24, 2009
• Time: 10:30am - 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Here are Aaron's slides. Further material on this topic can be found on Kenn Knowles's site.Abstract: A number of dependently-typed programming languages exist, but many either restrict expressiveness or require extensive user input to deal with the undecidability of type checking. Languages such as Cayenne, lambda-H, and Sage have instead used a "best-effort" attempt to deal with this undecidability by attempting to type check programs, but potentially failing to prove valid programs type-correct.One powerful (and undecidable) form of dependent typing is based on what are variously known as contract types, refinement types, or predicate subtypes. The lambda-H language uses refinement types alone, and Sage includes them as part of a "pure" type system that uses the same syntax to describe both terms and types.An interesting recent result (by one of my friends from Santa Cruz) shows that while type checking for refinement types is undecidable, a form of type inference is decidable. It has the interesting property that if the input program is well-typed, then it has the inferred type. However, the algorithm does not determine whether the input program is, in fact, well-typed. Because it only decides one part of the type inference problem, the authors refer to it as "type reconstruction" instead.I will talk about refinement types, existing techniques for checking them, and the basics of decidable refinement type reconstruction.

---

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Call for Proposals: CUFP 2009

Commercial Users of Functional Programming Workshop 2009:Functional Programming as a Means, Not an EndSponsored by SIGPLANCo-located with ICFP 2009Edinburgh, Scotland, 4 September 2009Galois is excited to promote this sixth annual event and encourages any interested in speaking at the workshop to send in a presentation proposal!  Whether you'd like to offer a talk yourself or you'd have someone in mind you'd like to nominate, please submit a proposal by 15 May 2009 via e-mail to francesco(at)erlang-consulting(dot)com or jim(dot)d(dot)grundy(at)intel(dot)com. Include a short description (approx. one page) of what you'd like to talk about or what you think your nominee should give a talk about.Do I have a presentation idea?If you use functional programming as a means rather than as an end (or could nominate someone who does), we invite you to offer to give a talk at the workshop. Talks are typically 25 minutes long but can be shorter and aim to inform participants about how functional programming plays out in real-world applications. Your talk does not need to be highly technical, and you do not need to submit a paper!What is the goal?The goal of the CUFP workshop is to act as a voice for users of functional programming and to support the increasing viability of functional programming in the commercial, governmental, and open-source space. The workshop is also designed to enable the formation and reinforcement of relationships that further the commercial use of functional programming.Tell me more!CUFP 2009 will last a full day and feature a keynote presentation from Bryan O'Sullivan, co-author of Real World Haskell. The program will also include a mix of presentations and discussion sessions varying over a wide range of topics.This will be the sixth CUFP;  for more information, including reports from attendees of previous events and video of recent talks, see the workshop web site: http://cufp.galois.com/.

Click to read more ...

Galois Tech Talk: Specializing Generators for High-Performance Monte-Carlo Simulation in Haskell

The March 10th Galois Tech Talks was delivered by Don Stewart on "Specialising Generators for High-Performance Monte-Carlo Simulation in Haskell."Here are the slides.

• Date: Tuesday, March 10, 2009
• Time: 10:30am - 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: We address the tension between software generality and performance in the domain of simulations based on Monte-Carlo methods. We simultaneously achieve generality and high performance by a novel development methodology and software architecture centred around the concept of a specialising simulator generator. Our approach combines and extends methods from functional programming, generative programming, partial evaluation, and runtime code generation. We also show how to generate parallelised simulators.We evaluated our approach by implementing a simulator for advanced forms of polymerisation kinetics. We achieved unprecedented performance, making Monte-Carlo methods practically useful in an area that was previously dominated by deterministic PDE solvers. This is of high practical relevance, as Monte-Carlo simulations can provide detailed microscopic information that cannot be obtained with deterministic solvers.

---

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Trustworthy Voting Systems

Accurate and reliable elections are a critical component of an effective democracy. However, completely secure and trustworthy voting procedures are difficult to design, and no perfect solutions are known. Ideally, a trustworthy voting system should guarantee both verifiability (the ability to prove that the counted vote matches the submitted ballots) and privacy (the inability to link the contents of a vote with the voter who cast it).These guarantees may now be achievable. Many researchers have proposed voting protocols that achieve verifiability and privacy in theory, and a few do so under assumptions that are satisfied by current election practices. Most of the protocols involve posting an encrypted version of the contents of every ballot in some public place (likely a web site), and depend on the properties of cryptographic operations to achieve privacy while allowing anyone to verify the final tally. Now that practical, secure voting protocols exist, the time has come to bring them into use. One existing solution that comes close to achieving these goals while retaining compatibility with current voting practices is the Scantegrity II system. It has the advantage that it can operate under current US election conditions, without requiring any modification to existing optical ballot scanners, and with very little change to the individual voting process. However, the software used in this system is only a prototype, with a number of shortcomings. Voter privacy depends on ability of a computer system to keep a key database completely secret, and accurate vote counting depends on the correct implementation of complex cryptographic algorithms. The software is tens of thousands of lines of code, and as with any other software of that size, many bugs certainly exist. We believe that the importance of trustworthy election results and the past lack of success in creating reliable solutions warrants a new approach to the design of voting systems. In particular, we advocate a class of techniques known as formal methods that allow us to make precise mathematical assertions about how software should behave, and determine whether it satisfies those assertions. Government agencies within the Department of Defense make use of formal methods to ensure the reliability of important computer systems, and the draft update to the development standards used by the Federal Aviation Administration, DO178C, includes provisions for the use of formal methods. Voting systems deserve similar care.

Click to read more ...