Last Thursday, the University of Bristol posted a press release and paper describing a way to exploit a bug in version 0.9.8g of OpenSSL and extract the value of a private key. The bug was known, and has been fixed in recent versions of OpenSSL (0.9.8g was released in 2007, and 0.9.8h fixed the bug […]
ZUC is a stream cipher that is proposed for inclusion in the “4G” mobile standard named LTE (Long Term Evolution), the future of secure GSM. The proposal is actually comprised several different algorithms: A stream cipher named ZUC, LTEencryption algorithm (128-EEA3), based on ZUC, LTEintegrity algorithm (128-EIA3), which is a hash function using ZUC as […]
Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers — extensions to SAT solvers with support for variables of non-boolean type — offer powerful automation for solving a variety of assurance […]
Copilot is an embedded domain-specific language designed by Galois, that allows you to generate assured, embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation). Lee Pike has written a tutorial on how to use Copilot to program an Arduino controller to play “Jingle Bells”. Read the full tutorial on […]
During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a “Functional Programming in Industry” impromptu workshop. The following are slides I presented on Galois’ experience building a business using our functional programming expertise, in particular, Haskell. The talk describes three case studies where “functional thinking” helped shape the solution to […]
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
John Launchbury presented the Orc language for concurrent scripting at the Haskell Workshop, 2010 in Baltimore.
Concurrent Orchestration in HaskellJohn LaunchburyTrevor Elliott
The talk slides are available in PDF or online.
We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Orc DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to establish and demonstrate algebraic properties satisfied by the combinators.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!The talk will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
Typing DirectoriesDetails:
Abstract: PADS describes the contents of individual ad hoc data files, but has no provisions for describing collections of files, i.e., directories. In this talk, I explore examples where having a declarative description of directories as well as files would be useful, including websites, source code trees, source code control systems, operating systems, and scientific data sets. As part of this exploration, I identify essential features of a directory description language and useful tools that might be produced from such a description. I end with a series of questions about how such a language might most easily be implemented in the context of Haskell.This is joint work with David Walker and Kenny Zhu.Bio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher is a Principal Member of the Technical Staff at AT&T Labs Research and a Consulting Faculty Member in the Computer Science Department at Stanford University. Kathleen’s research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data, including the Hancock system for efficiently building signatures from massive transaction streams and the PADS system for managing ad hoc data.Kathleen is an ACM Distinguished Scientist. She has served as program chair for FOOL, CUFP, and ICFP. She is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), Co-Chair of CRA’s Committee on the Status of Women (CRA-W), and an editor of the Journal of Functional Programming. She is currently serving on the CRA Board.
The eight queens puzzle asks how to place eight queens on a chess board such that none of them attacks any other. The problem easily generalizes to n queens, using an nxn board. In this post, we’ll see how to solve the n-Queens puzzle in Cryptol, without lifting a finger!
It is easy to see that any solution to the n-Queens puzzle will have precisely one queen on each row and column of the board. Therefore, we can represent the solution as a sequence of n row numbers, corresponding to subsequent columns. For instance, the board pictured below (taken from the wikipedia page), can be represented by the sequence
3 7 0 2 5 1 6 4
recording the row of the queen appearing in each consecutive column, starting from the top-left position. (And yes, we always count from 0!)
I can never shuffle cards properly. They seem to go every which way when I try, and a perfect random shuffle seems nigh-impossible to achieve, even though the experts claim it takes a mere 7 moves. (The mathematical argument is surprisingly quite technical.) Luckily, we shall concern ourselves with a much simpler problem today: How many perfect out-shuffles does it take to restore a deck back to its original order? We’ll throw in a couple of variants of the problem for fun, but rest assured that we’ll let computers do the work. And, of course, we’ll use Cryptol to help us along the way.
According to wikipedia, a riffle (or dovetail) shuffle goes like this:
… half of the deck is held in each hand with the thumbs inward, then cards are released by the thumbs so that they fall to the table interleaved. Many also lift the cards up after a riffle, forming what is called a bridge which puts the cards back into place…
Well, I read that a couple times, and watched a couple of videos on the internet showing how to do it, but no luck so far. Luckily, this sort of shuffling is quite easy to express programmatically, and Cryptol has the right abstractions to code this in a couple of lines.
The first step in the shuffle is bisecting the deck into two equal halves:
bisect : {a b} (fin a) => [2*a]b -> ([a]b, [a]b);bisect xs = (take (w, xs), drop (w, xs))where w = width xs / 2;
We simply compute the mid-point, and divide the given sequence xs into two, by take‘ing and drop‘ping the correct amounts from the input sequence. In fact, the type of bisect is more interesting than its definition: It succinctly captures the following four facts:
The ability to express precise size/shape-polymorphic properties using types is one of the strengths of Cryptol.
Once the deck is split into two, we proceed by picking the cards alternatingly from each half. We have two choices: We can either start with the first half, or the second. If you start with the first half, that’s called an out-shuffle. If you start with the second half, then it’s an in-shuffle. These two functions are actually quite easy to code in Cryptol:
outShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;outShuffle xs = join [| [x y] || x <- fh || y <- sh |]where (fh, sh) = bisect xs;inShuffle : {a b} (fin a) => [2*a]b -> [2*a]b;inShuffle xs = join [| [y x] || x <- fh || y <- sh |]where (fh, sh) = bisect xs;
The definitions are almost identical, except for the order in which we put the cards from the halves (fh and sh) together. In the outShuffle, the first card in each pair comes from the first-half. In the inShuffle, it comes from the second half. Easier done than said! Let’s make sure they behave as we expect:
Cryptol> bisect [1..8]([1 2 3 4], [5 6 7 8])Cryptol> outShuffle [1..8][1 5 2 6 3 7 4 8]Cryptol> inShuffle [1..8][5 1 6 2 7 3 8 4]
Good! It’s interesting to see what happens when we apply bisect to an odd-length sequence:
Crytpol> bisect [1..9]In a top-level expression: with inferred type:{a} ([a][4],[a][4])encountered the following unresolved constraints:fin a2*a == 9
Cryptol is basically telling us that there is no a such that 2*a is 9, resulting in a type-error. Note that this is a static-check before you run your program! In other words, if your program type-checks, then you can rest assured that whenever you call bisect, it is guaranteed to get an even-length sequence as its argument. Strong static typing and size-polymorphism of Cryptol really pays off in this case!
Before proceeding to the properties of shuffles, we need one last notion: The application of a shuffle repeatedly to a given input, yielding an infinite sequence of transformations:
iterate : {a} (a -> a, a) -> [inf]a;iterate (f, x) = [x] # iterate (f, f x);outShuffles, inShuffles :{a b} (fin a) => [2*a]b -> [inf][2*a]b;outShuffles xs = iterate(outShuffle, xs);inShuffles xs = iterate(inShuffle, xs);
The high-order function iterate gives us the infinite sequence of results of applying a function to a value over and over. We simply use this helper to define outShuffles and inShuffles to apply the corresponding functions indefinitely to their input. Note that the resulting type shows that we get an infinite sequence as output, as indicated by the size inf.
It turns out that if one applies 8 out-shuffles to a deck, a remarkable thing happens: Nothing! The deck goes back to its original order! This is a bit hard to believe, and harder to realize using a real deck of cards. (A friend of mine says he saw it done at college once by hand, but I’m yet to meet anyone who can do this successfully so far!)Well, the good thing about programming is that we can manipulate the sequences at will, without fear of messing up the cards. Even better, we can assert the above claim as a theorem in Cryptol:
type Deck = [52][6];outShuffle8 : Deck -> Bit;theorem outShuffle8: {deck}.outShuffles(deck) @ 8 == deck;
We have defined a Deck to be a sequence of 52 things, each of which is 6-bits wide, which is more than enough to cover all the 52-unique elements that appear in an ordinary deck. (6-bits can encode 64 values, so we have 12 unused elements.) The theorem simply states that the 8’th element of the infinite sequence of outShuffle applied to an arbitrary deck gives us back the original deck.Let’s ask Cryptol to prove this theorem: (Cryptol’s symbolic and sbv backends can perform these proofs, so we first set our mode accordingly below.)
Cryptol> :set sbvCryptol> :prove outShuffle8Q.E.D.
Voila! The proof completes instantaneously, with almost no time elapsed. (This might be surprising at first, since the input space to the theorem has 52*6 = 312 bits, which is quite large. However, we note that the theorem is actually fairly easy to prove since all shuffling does is a mere re-ordering of things with no specific computation; which is easy to manipulate symbolically for Cryptol’s proof engine.)
Can we reverse a deck of cards using outShuffle‘s? Turns out that this cannot be done. In particular, an outShuffle never moves the first element of the deck anywhere:
outShuffleFirstCard : Deck -> Bit;theorem outShuffleFirstCard: {deck}.outShuffle deck @ 0 == deck @ 0;
We have:
Cryptol> :prove outShuffleFirstCardQ.E.D.
Since the first card remains stationary, there is no way to reverse a deck of cards by just using outShuffles.How about with inShuffle? Turns out the magic number is 26 for reversing a deck of cards in this particular case:
inShuffle26Rev : Deck -> Bit;theorem inShuffle26Rev : {deck}.inShuffles(deck) @ 26 == reverse deck;
Again, the proof is immediate:
Cryptol> :prove inShuffle26RevQ.E.D.
If 26 in-shuffle’s reverse the deck, then 52 of them will restore it back. Here’s the corresponding theorem:
inShuffle52 : Deck -> Bit;theorem inShuffle52: {deck}.inShuffles(deck) @ 52 == deck;
Again, the proof is immediate.
There is one more variation on the shuffle that we w
ill consider. The mongean shuffle picks the even and odd numbered elements, reverses the odds and adds the evens at the back. For instance, given the sequence: 0 1 2 3 4 5 6 7 8 9, we first construct two sub-sequences: The even index elements: 0 2 4 6 8, and the odd ones 1 3 5 7 9. We then reverse the latter to get 9 7 5 3 1, and append the former, obtaining: 9 7 5 3 1 0 2 4 6 8. Luckily, the Cryptol definition is much easier to read:
monge xs = reverse odds # evenswhere { w = width xs;evens = xs @@ [0 2 .. (w-1)];odds = xs @@ [1 3 .. (w-1)]};monges xs = iterate(monge, xs);
With a monge shuffle, it takes 12 rounds to restore a deck:
monge12 : Deck -> Bit;theorem monge12: {deck}. monges(deck) @ 12 == deck;
We will leave it to the reader to construct the argument that no sequence of monge shuffles would reverse a deck. (In particular, one can prove that the 18th element from top will never move in a deck of 52. Proving this theorem in Cryptol is again quite trivial.)
The attentive reader might worry that our Deck type does not quite correspond to a deck-of-cards. This is indeed the case. There are two discrepancies. First, as we mentioned before, our decks can represent 64 elements, while a deck of cards has only 52 distinct cards. On the plus side, this just makes our theorems “stronger,” since we allow for more cards then possible. More importantly, the properties are intended for decks that have no-repeating cards in them. (That is, every card occurs precisely once.) But our theorems apply to arbitrary deck‘s, even those that have repeating elements in them. Again, this just makes our theorems stronger, as the unique-sequence cases directly follow from them. We can rest assured that our proofs are conclusive, even though our model of playing-cards is not perfect.
Free evaluation licenses of Cryptol are available at www.cryptol.net. The Cryptol source code for shuffling cards is also available as well.
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.