Looking Out To Sea

I’m in a new job. I’ve done one week, so my life has mostly been on hold while I work out how things will fit together. I’m working for Honeywell Security writing embedded software. Similar to before but in alarm systems instead of networking.

The job requires a hefty commute — at least two hours each way if things go well, but between delayed trains and poor weather it’s sometimes an extra half hour on top of that. Which means I get up at 5.30, leave the house before 6.30 and get home in the evening around 7 o’clock. You can see why the rest of my life has been a bit quiet. I’m having to rethink how I look at the week. The arrival of the weekend is important and precious!

I’m still learning the ins and outs of work but the people are all very friendly and helpful, which makes the travelling more bearable. Spending hours travelling to and from a hateful job would be horrible. I spend an hour on the train each way which has given me more time for other things. I’ve been splitting my travelling activities, so that in the morning I read the freebie Metro for a bit and then do some “thinking” to limber up for the day. Recently I’ve been doing simple program calculation exercises, deriving the fusion rules for fold/unfold or map/map and so on. I’m really interested in the idea of deriving correct and efficient programs from executable specification.

(Just to show you what I’m talking about, this is the fold/unfold fusion rule. Let us say there are two functions, foldr and unfoldr defined as follows:

foldr f z     [] = z
foldr f z (x:xs) = f (foldr f z xs)
 
unfoldr g s = case g s of
                Nothing     -> []
                Just (x,s') -> x : unfoldr g s'

The function foldr combines a list of elements according to the function f and unfoldr creates a list of elements from the seed s. We might use foldr to define a product function which combines the elements of the list by multiplying them together:

product = foldr (*) 1

And we might create a list of elements from 1 to n with an unfold.

enumTo n = unfoldr step 1
  where step s = if s>n then Nothing else Just (s, s+1)

The observant reader will have noticed that combining these two separate functions will give us factorial, the product of numbers from 1 to n — first we create the numbers 1 to n, then we multiply them all together.

factorial = product . enumTo

The inefficiency is that enumTo works on producing a list which is consumed by product. The elements are inserted into a list only to be removed straight away. Can we omit the redundant list production? It turns out we can, and we can do it for all cases where foldr operates on the result of unfoldr. The product and enumTo are specific instances of a general method which we can use to fuse production and consumption of values.

This fusion rule can be demonstrated by algebraic manipulation of the programs we’ve defined so far. We’ll call the unfoldr and then foldr by the name hylo, with the naive implementation shown:

hylo f z g = foldr f z . unfoldr g

The equational style here facilitates some nice rearrangements which help to assert their correctness from step to step. Let’s see how this works — each line will be justified by some comment in braces:

  hylo f z g s
= { definition from above }
  foldr f z (unfoldr g s)
= { definition of unfoldr }
  foldr f z (case g s of
                  Nothing     -> []
                  Just (x,s') -> x : unfoldr g s')
= { push foldr into result }
  case g s of
       Nothing     -> foldr f z []
       Just (x,s') -> foldr f z (x : unfoldr g s')
= { foldr on empty lists }
  case g s of
       Nothing     -> z
       Just (x,s') -> foldr f z (x : unfoldr g s')
= { foldr on non-empty lists }
  case g s of
       Nothing     -> z
       Just (x,s') -> f x (foldr f z (unfoldr g s'))
= { definition of hylo }
  case g s of
       Nothing     -> z
       Just (x,s') -> f x (hylo f z g s')

Each step should be clearly equivalent to the one before and the one after, but by the end we have a definition for hylo which doesn’t construct a useless list.

hylo f z g s = case g s of
                 Nothing     -> z
                 Just (x,s') -> f x (hylo f z g s')

Naturally we can use the original definitions of product and enumTo to create an optimised factorial using this logic. The result is that factorial doesn’t create a redundant list either:

factorial n = hylo (*) 1 step
  where step s = if s > n then Nothing else Just (s,s+1)

I think this is beautiful result despite its obvious simplicity. However this has been a long digression, so I’ll stop now. But if you found it interesting I encourage you to check out work on “program calculation”, “program derivation”, “algebra of programming”, “origami programming” and so on.)

My evening journeys have been spent unwinding with a book, though the evening trains are noisier. I’m reading Brighton Rock right now and it’s good though the story makes me feel quite uncomfortable at times. One of the characters seems close to doing something wild and dangerous and it’s a fight between “must find out what happens” and “can’t bear to read any more” on a daily basis.

I hope week two will be easier and I will start to feel like my routine is falling into place. Watch this space.

This is the third part of my slow examination of Kiselyov and Shan’s Lightweight Static Capabilities paper. Start at the the beginning and then read part two to put this part into context.

Section 3 of the paper uses the same technique from Section 2 and adapts it to tackle a larger and more interesting problem: array bound checking. To motivate the problem they follow in the footsteps of the dependent type literature by implementing binary search with statically-checked “safe” array lookups.

To explain the approach they use we’ll start with an unsafe implementation that uses runtime bounds checking on each index.

bsearch :: (Ord a) => (a -> a -> Ordering) -> a -> Array a -> Maybe (Int,a)
bsearch cmp key arr = go 0 (length arr - 1)
  where go lo hi = if hi >= lo
                      then let midpoint = lo + ((hi - lo)`div`2)
                               curvalue = arr ! midpoint
                           in case cmp key curvalue of
                                  LT -> look lo (m - 1)
                                  EQ -> Just (m, curvalue)
                                  GT -> look (m + 1) hi
                      else Nothing

The index operation (!) checks at runtime to see if the supplied index is within the bounds defined by the array (we still have to catch an exception, which I haven’t shown here, but at least it won’t blow everything up). This check is not necessary if we can prove that the index will always be in range.

The general approach outlined in Section 2 was to brand “safe” operations and types which go together. Once a list had been branded non-empty (ie had type FullList) it could be freely passed around and later safely destructured into head and tail without worry.

In the case of lists the values were branded “safe” and the head/tail operations could only work on “safe” values. The head operation is analogous to indexing the 0th element in an array. If we were to extend the list approach to arrays we would need a deref0 for the 0th element, deref1 for the 1st element and so on. This is both unwieldy and needlessly restricts the type of indexing possible.

The solution proposed by the paper is a set of “safe” indexing operations which only work when both the array and the index are branded as being compatible. An index is compatible with an array if it is within that array’s bounds.

get :: BrandedArray b a -> BrandedInt b -> a

The type variable b here is a phantom type which brands arrays and indices. The get operation can only be used if the same brand is applied to both array and the index.

Initially the only “safe” array indices are the offsets of the upper and lower element. The brands for an array are created alongside the upper and lower index in one operation, providing the assurance to the type system that whatever type b represents it is identical for these three values:

brand :: Array -> (BrandedArray b a, BrandedInt b, BrandedInt b)

(In fact this is not the proper type signature. The proper signature is reproduced below, with existential quantification over the branding type b and continuations for passing/failing conditions. This signature is just a gentle introduction to get the idea across)

Further operations can be created with transformations on the provided indices: increments, decrements and midpoints.

Whatever b is here it’s the same type, but next time brand is called b may well be a different type. The type system can’t unify them since it doesn’t know the type — it’s never specified. So only indices created alongside the branded array can be used with it, since only in that situation can the type checker be sure that the type of b matches.

This seems a powerful use of phantom types and it’s one I’d never seen before. The paper uses the phrase “type eigenvariable” at this point, which I’m not familiar with but it’s such a nice phrase that I’ll have to keep an eye out for it.

As before the type constructors to enforce this safety are hidden and only accessible under specific and well-guarded conditions.

-- Not exported!
newtype BrandedArray b a = BrandArray a
newtype BrandedInt   b i = BrandInt i
 
brand :: Array -> (forall b. (BrandedArray b, BrandedInt b, BrandedInt b) -> w)
               -> w -> w
brand arr cont stop = if lo <= hi
                         then cont (BrandArray, BrandInt lo, BrandInt hi)
                         else stop

The user provides functions to deal with the two cases that the bounds are valid and invalid. This same pattern follows through to other parts of the implementation: condition checking is done internally and the user provides functions to deal with various cases. This keeps some of the constraints (like the existential quantification over b, the brand type) wrapped up. If the user tries to subvert this the type checker objects:

Inferred type is less polymorphic than expected
  Quantified type variable `b' escapes
In the second argument of `brand', namely `Just'
In the expression: brand testarray Just Nothing
In the definition of `it': it = brand testarray Just Nothing

In order to implement the rest of binary search over arrays some arithmetic functions on indices are introduced. These functions exist inside the trusted kernel so some effort is made to ensure they are correct. They also require passing/failing functions for operations that may fail (such as finding the successor of a valid index: the successor may be out of bounds):

-- If i1 and i2 are within bounds then their midpoint
-- is within bounds.
bmiddle :: BrandedInt b -> BrandedInt b -> BrandedInt b
bmiddle i1 i2 = BrandInt (i1 + (i2 - i1) `div` 2)
 
bsucc :: BrandedInt b -> BrandedInt b
                      -> (BrandedInt b -> w)
                      -> w -> w
-- If i is less than the upper bound we use continue calculation
-- with the inside else we fail with outside.
bsucc (BrandInt upper) (BrandInt i) inside outside = 
    let i' = i + 1
    in if i' <= upper then inside (BrandInt i') else outside

There is also a predecessor function which works analogously. First we need to rework the binary search for this style of programming:

bsearch :: (Ord a) => (a -> a -> Ordering) -> a -> Array a -> Maybe (Int,a)
bsearch cmp key arr = brand arr find Nothing
  where find (barr,lower,upper) = go lower upper
    where go lo hi = let m = bmiddle lo hi
                         x = unsafeGet barr m
                     in case cmp key x of
                        LT -> bpred lo m (\i -> go lo i) Nothing
                        EQ -> Just (unbrand m, x)
                        GT -> bsucc hi m (\i -> go i hi) Nothing

On each iteration of the algorithm finding the value at the midpoint is always a safe operation provided the two arguments are safe. Incrementing or decrementing the upper/lower bound might fail if the index goes out of range, but this check can be considered part of the end condition, ie the search finishes unsuccessfully anyway if the index goes off the end because it’s an indication that the value we’re looking for is not stored.

The call to unsafeGet is, in fact, safe, since the index m is guaranteed to be in range for this array. No runtime checks are required over those needed to indicate the end condition. As before this problem is always dealt with formally using a similar mechanism for the empty-list problem, using Strict and Lax languages and mappings from one to the other. I’ll look at that next time.

This is part 2 of a series of posts looking at the paper Lightweight Static Capabilities by Kiselyov and Shan. Part 1 can be found here.

The next section of the paper is more theoretical. The authors introduce two notional languages, Strict and Lax, and their typing mechanisms. Strict has a “fancy” type system which specifies two list types (List and List+) and only the latter type can be deconstructed with head and tail functions. The List+ type can only be created by a special nonempty conversion, which cannot be applied to empty lists.

The Lax language has no such advanced typing facility and will happily accept nonempty(nil) as a legal construct. This language is more like a traditional functional language with a possibly-empty list type. In terms of typable operations Strict defines a smaller set than Lax, and every legal Strict program is a legal Lax program too. The authors define a mapping from Strict to Lax programs to allow embedding a statically safe program in Haskell, ML, etc.

This embedding is ultimately what we always attempt to do when programming. The set of things which the compiler will accept is necessarily larger than the set of things which will get us the right answer. Type systems aim to constrain the “acceptable” set slightly though there is still plenty of scope for bugs. :-) Some programming languages make it easier to write programs which are dangerously but subtly wrong. Using the full capabilities of a language like C all the time is incredibly foolhardy: not every situation demands pointer arithmetic. If we can use the type system to wall off “dangerous” code then all the better. Another example is the use of IO actions or unsafe* operations in Haskell. These are often used only where necessary in the former case, or walled off in an opaque module in the latter case. This walling-off allows us to concentrate our verification efforts to areas which can cause the most problems.

The resulting “embedded” code is the trusted kernel mentioned in the previous post. The reduction rules defined for Strict and Lax are contained in this kernel. The reduction rules for the non-empty list case are:

head (nonempty (cons E1 E2)) -> E1
tail (nonempty (cons E1 E2)) -> E2
indeed nil E1 E2             -> E1
indeed (cons E E') E1 E2     -> E2 (nonempty (cons E E'))

The first two rules define the operation of head and tail on a non-empty list. These operations aren’t defined for empty lists. The second two rules show how the non-empty type is constructed if the list is truly non-empty. Notice the similarity between indeed and Haskell’s maybe function (with arguments rearranged):

indeed :: List a -> b -> (FullList a -> b) -> b
maybe :: Maybe a -> b -> (a          -> b) -> b

The maybe function forces the user to deal with all cases in the option type by requiring functions and default values for each case. The indeed function goes one step further by not allowing any other way to take apart the list type — in order to use head and tail you have to convert the List to a FullList and only indeed can do that.

In the spirit of the maybe function for Maybe types and the either function for Either types it would seem sensible to have a list function for List types, which would take a function for each case suggested by a list. After a bit of reflection I think this is the fold, or rather maybe and either are specific folds.

Which all suggests that the toy example provided (reversing a linked list) can be safely recreated using a fold. If we look again at the safe version defined in the previous post we see two cases we have to deal with:

reverse :: List a -> List a -> List a
reverse xs acc = case full xs of
            Nothing -> acc
            Just ls -> reverse (tail ls) (cons (head ls) acc)

Stripping away all the plumbing stuff that’s going on here, we have two vital bits:

1. The return of the accumulator when the list is no longer non-empty, ie is empty.
2. Consing the head of the list onto the accumulator at each stage that the list is non-empty.

Step 1 is done automatically by the fold: it lets you iterate over values without being concerned about them running out. Step 2 is just the cons operation we know, with the order of arguments reversed. To actually reverse a list we supply an empty accumulator.

reverse in = foldl combiner acc in
  where combiner xs x = cons x xs
        acc = []

We know we can define this simple function as a one-liner but not all functions are as simple. The next section looks at array indexing operations. The motivating example this time is binary search over arrays — checking that all indexing operations remain in-bounds and that these constraints are ensured by the type system. By contrast with list reversal a binary search deals with several separate elements (the array, the lower and upper index) which cannot be hidden completely if we are to allow general array operations.

I started to look at the Lightweight Static Capabilities paper over lunch on Friday. This is far too big an paper to consume in half an hour and I’m a long way from understanding it all. I thought the best way to increase my understanding was to write down my thoughts on and understanding of each section as I come to it. (The examples here are given in Haskell-like syntax, with fewer obscure operators. Conseuqently I’ve used the type name List a instead of [a] and cons instead of infix :.)

The area the paper looks at is labeled “lightweight dependent typing” — dependent typing without dependent types, essentially. Dependent type systems allow the programmer to specify types based on the values, so the programmer can ensure that lists will necessarily be non-empty and denominators necessarily non-zero, among other useful examples. The paper looks at ways of creating type safe “capabilities” without dependent types.

I will take the paper a little bit at a time, and as I read on I might have to correct previous misreadings/misinterpretations. The first motivating example given on page 2 provides a program to reverse a list, building up the result in an accumulator.

reverse :: List a -> List a -> List a
reverse ls acc = if nil ls
                    then acc
                    else reverse (tail ls) (cons (head ls) acc)

The standard list destructors head and tail are partial functions. They are not defined for the empty list and will produce a runtime error if accidentally applied to the empty list. For this reverse function we can be reasonably certain that it won’t blow up at runtime, but it’s a very simple function and we can’t get the same assurances in all situations. Let’s call these standard head and tail functions by more explicit names:

unsafeHead :: List a -> a
unsafeTail :: List a -> List a

In order to provide static guarantees that all uses of head and tail are safe a new type called FullList is introduced which is a rebranded standard list type. The key element is that head and tail can only operate on FullList types, and a guarantee is provided that values in this type are non-empty lists. With this static assurance we can actually use our unsafe functions from earlier:

-- unfull converts a FullList to an ordinary List type
head :: FullList a -> a
head = unsafeHead . unfull
 
tail :: FullList a -> List a
tail = unsafeTail . unfull

The FullList type becomes a one-use token which the value has when it moves through the program. This token can only be created in one place (which we can lock inside a separate module). We can easily control under what conditions this token is assigned:

module (FullList, unFull, full) where
 
newtype FullList a = Full { unFull :: List a }
 
full :: List a -> Maybe (FullList a)
full ls = if null ls then Nothing else Just (Full ls)

To verify that head and tail are always “safe” we must only verify that a FullList is always non-empty. The paper goes deeper into the formal verification than I’m comfortable talking about (at least at the moment) but it should be reasonable to say that there is only one line of code, the definition of full, which needs examined.

This is the kernel of trust concept that the paper revolves around. Shrinking down this kernel means it’s easier to examine and verify; and from there the type system extends our trust to the rest of the program.

From the user perspective, the type system forces us to check that lists are not empty before invoking head or other unsafe list operations:

reverse :: List a -> List a -> List a
reverse xs acc = case full xs of
            Nothing -> acc
            Just ls -> reverse (tail ls) (cons (head ls) acc)

Ideally we’d be doing this anyway so there isn’t a greater burden — but it does provide us with compilation errors if we forget to do it. (From personal experience the use of an option type like Maybe makes it much harder to forget these things, even before getting the compiler error. And calling fromJust or other unsafe extraction method feels immoral.)

This takes us up to Section 2.1, with only one omission. The paper at this point switches from explicit wrapping and unwrapping of option types to continuation-passing style. The option types are straightforward but slow things down. Depending on how things go I might follow suit and use continuation-passing from here on, but it might prove a better learning experience to convert to option types. We’ll see when I come to write up the next section.

Severely snowed out today so SICP study group was cancelled. I’m using the time in the house to make stock with the bag full of lamb bones and bits that have been sitting in the freezer for many months. I think I will make some kind of soup with it later, preferably one with lots of chunky vegetables and other interesting bits. I’ve also got a bunch of beetroot in the fridge which I intend to make into beetroot and chocolate cake, because it was so tasty last time I made it. (And I want to do it in a cooler oven since 190°C blackened the outside without cooking through when I made it before. That was the only occasion when the skewer test has been useful to me.)

Back to the topic of the study group. Reading SICP is deceptively easy at times. Each step is a simple progression from the last, such that each idea seems obvious and trivial. Then suddenly some trivial new concept makes no sense at all and you find yourself backtracking through pages of explanation to find some firm handhold from which to start moving forward again. Most of the time I feel that I’m not learning anything but I realised today that some things which were not intuitive in the past are now familiar and natural. I was reading The Arrow Calculus and realised that I could understand all of the notation and type rules for lambda calculus and arrows given. It was the environment stuff in particular that felt “obvious” in the way that it wouldn’t have in the past, and I’ve been doing a lot of interpreter writing and environment-jigging in recent weeks with SICP. It’s all coming together.

Earlier today our little SICP study group agreed to start on Chapter 3 for our next meeting. There are five chapters in total so we are past the halfway mark and it’s been pretty interesting so far. To recap the recent stuff:

• Representing data structures as functions, and data as functions. Specifically, calculating with Church numerals and simulating cons, car and cdr without built-in operations.
• Manipulation of code as data, including symbolic differentiation of simple algebraic formulae. Converting “3x²” into “6x” with relevant simplification and grouping of symbols.
• Some straight-up data structure work — ordered lists, trees, sets — and using them to implement Huffman encoding.
• Organising multiple interacting systems, in this case a generic arithmetic package which works (almost) seamlessly on integers, rationals, reals, complex numbers and finally polynomial terms. Using this as a way of discussing functional and object-oriented design and introducing the expression problem.

I can definitely say that this last section, building a multi-module (for some definition of module) system made me really miss static types. Not being able to tell where functions were defined and called with different arities, or were using different symbols, until the problem manifested at runtime, was infuriating. The book is very interesting but the language is not to my taste. :-)

For comparison, here’s Yaron Minsky talking about using Ocaml for large scale programming:

Effective ML from Yaron Minsky on Vimeo.

In case you didn’t see his comment, I just wanted to promote Andrew’s answer to my question to the front page. I had wondered why my dividing-by-two techniques had worked to find the answer to the second part of the Cyber Security Challenge. The explanation is quite obvious when written in full.

The input sequence was a series of 8 bits which had been permuted in some way. According to the published solution they had been rearranged so that the right-most bits had been looped around and pushed onto the left side:

6 7 8 1 2 3 4 5

The recommended solution was of course to take those three and move them back round to the right hand side:

1 2 3 4 5 6 7 8

My accidental solution relied on two features of the problem. First, as I said previously, the hexadecimal encoding could be reordered before decoding. Since each hex number represents 4 bits, we’re going to reorder around the middle:

6 7 8 1 : 2 3 4 5

If we swap these 4-bit sequences first, we get something which is very close to the desired sequence:

2 3 4 5 : 6 7 8 1

The next step I performed was division-by-two. In binary this is represented by shifting all the numbers one place to the right. (Think of dividing by ten normally — you just shift the decimal point one place to the left.) When we do this right-shift the right-most digit disappears, and a left-most digit is created which is always zero in our case. I’ll mark this place with a # symbol.

# 2 3 4 5 6 7 8

We’ve almost got a full understanding of the solution here, but one problem remains. My method and the official method are nearly identical, except for the left-most bit:

1 2 3 4 5 6 7 8 <-- official solution
# 2 3 4 5 6 7 8 <-- my solution

We don’t know what any of the bits 1–8 represents, but we know that # is always a zero. So my solution “works” when bit number 1 is zero. And it just so happens that ASCII, the standard way of encoding simple characters in binary, only uses the 7 bits on the right. The left bit, number 1, is always 0 for simple text encoding.

If the message had been encoded in some extended ASCII format that uses all 8 bits my method would have failed. For the general case, bit 1 is only zero half the time!

This second part of the problem was more difficult, though the solution is much shorter to present. The input message looks like this, in part:

68edcdec4e2c8eae8d2c8e2dedcd6e04d2042fedae52ceac
04ccedaecd8c042ccd8c046cedad0e8dac8eac8c048e0dac

Under the assumption that each pair of characters represents a byte, we split the stream into pairs.

splitStream = splitEvery 2

Of course each pair isn’t actually a hexadecimal number, though it looks like one. It’s a string of characters, so we need to turn it into something the computer will recognise as a number.

Now, there’s a robust, I’m-a-serious-engineer way of doing this and then there’s the way I chose, which is to prefix all the strings with “0x” and use the read routine. The Read typeclass is not meant to represent a robust parsing mechanism but since this is a one-shot thing I think we’ll both just ignore it, yeah?

hexToInt :: String -> Int
hexToInt = read . ("0x" ++) -- ouch!

Having read in our number I tried to do what I did in the previous exercise and print it out, which produced complete nonsense. Then I decided that reversing the string before converting it to numbers would be helpful. I did that, but the result was still nonsense, just of a different shade.

Then I decided that my resulting numbers were a bit large. The number which represent capital A is 65, and I was getting numbers in the 200 range. Then I realised, “all these numbers are even, aren’t they?” So I divided the whole lot by two.

Outputting that message gave me a backwards English message. Aha! It’s close but there’s something wrong. I threw in another “reverse” statement and got an answer. At this point I noticed I had two reverse statements — one at the beginning and one at the end. This seemed like it would be the cause of my problems so I removed them both and, Robert’s your father’s brother, I was back to gibberish again.

What happened? What I had failed to realise was that when I had reverse my original message I had done so before splitting into pairs of characters. So ABCD becomes DCBA. After splitting this is [DC,BA]. If each pair is converted into a printable character, represented by f(XY), then the result is [f(DC),f(BA)]. I then reversed the message to get [f(BA),f(DC)].

If I didn’t do any reversing but went through the same splitting and conversion process, I got [f(AB),f(CD)]. Look — f(AB) is not the same as f(BA)! By reversing the list before splitting and again after conversion, I was implicitly reversing the order of the characters in each pair.

Obviously I had to reverse only the pairs after they’d been split, rather than the whole list at the beginning and end. If I do this then print the result I get an answer which is close to right.

byteToChar = chr . flip div 2 . hexToInt . reverse
message = map byteToChar . splitStream
 
loadfile = (head . lines) `fmap` readFile "hexstring.txt"
main = loadfile >>= putStrLn . message

The resulting message is:

Congratulations youve found and completed the REAL challenge. Your win code is cyb3r=s3cur1ty*ch@ll3nge+26-07-2010.

Please email this code to our team at media@cybersecuritychallenge.org.uk. If youre the first person to do so, and can prove you meet the eligibility criteria (British citizen currently resident in the UK) we will be in touch to advise how to claim your prize. Well done and good luck in the Cyber Security Challenge competitions taking place throughout the rest of the year.

There are a few infelicities which are explained by the official solution. My divide-by-two technique is not the proper approach so I think some of the characters get lost in the decryption process. But as the saying goes, close enough for government work!

The solution states:

The challenge was based on a bitshift operation applied to a string, here each byte’s “3 least significant bits” have been added to the left side of the byte (making them the most significant bits respectively)

Assuming we have bits one to eight:

1 2 3 4 5 6 7 8

what I did was divide everything by two, which we do in binary by shifting everything to one side so the least significant bit disappears. We fill the opposite edge with a zero here:

0 1 2 3 4 5 6 7

What the solution demands is to rotate the bits like so:

6 7 8 1 2 3 4 5

I am still not sure how it is that my solution matches so neatly with their own. Answers on a postcard.

If I hadn’t stumbled on a solution like this, the sensible approach might have been to produce a histogram of common characters. In this case, the most commonly used character encoded the space, followed closely by “e”, the most common letter in standard English texts. From there it would have been a bit of a slog to produce the result but it could be done.

The two other solutions I have found both use the official method without problems. I suspect it’s got something to do with default word lengths (8 bit versus 32 bit) and signed integers, though I’ve not thought deeply on the issue.

The first part of the Cyber Security Challenge requires you to decode a long stream of letters, numbers and symbols into something coherent. This was by far the easiest part of the challenge. The symbols look like this:

/9j/4AAQSkZJRgABAQEAYABgAAD/4QBaRXhpZgAATU0AKgAAAAgABQMBAAUAAAABAAAASgMDAAEA
AAABAAAAAFEQAAEAAAABAQAAAFERAAQAAAABAAAOxFESAAQAAAABAAAOxAAAAAAAAYagAACxj//b
AEMACAYGBwYFCAcHBwkJCAoMFA0MCwsMGRITDxQdGh8eHRocHCAkLicgIiwjHBwoNyksMDE0NDQf

This is only the first three lines — there’s 362 lines of this. The most important bit is that the last line ends in a = sign. This symbol is used for padding out messages when they are encoded in Base 64 format, so if any string has an equals symbols on the end it’s worth seeing what happens if you decode it as if it were Base64. (The truth of the matter is that by the time my mate Rich had told me about this challenge he’d already decoded the image so I didn’t do any of this stuff!)

Thankfully there are plenty of programs that will do the decoding for you, and the resulting file is a JPEG file. Brilliant:

This is XKCD comic number 538, with a subtle difference. Round the outside of the image there is an uneven dotted border. This isn’t in the original comic, and it looks irregular which suggests that it’s not just a pretty pattern but that it encodes some further information.

For the next stage I converted the image to PNG format because it was the easiest format to load and process.

The first part we need to do is load the image file and extract all the bytes from the actual image part, ignoring any metadata. The PNG file is represents a 24 bit colour image, with each component (red, green and blue) stored as an 8 bit number from 0–255. We just return the whole thing as a long list of bytes, starting at the top left and scanning left to right, top to bottom. It’s not efficient but it’s very simple to reason about because we don’t need to think about array locations.

getimage :: IO [Word8]
getimage = do
  (Right img) <- loadPNGFile "decode.png"
  getElems (imageData img)

The long list may be conceptually simple but it’s not representative of the structure of the image. Since each pixel is represented by 3 consecutive numbers we want to gather those numbers together, so we can start dealing with them as pixels. Thus we convert [r,g,b,r,g,b,r,g …] into [[r,g,b],[r,g,b],…]

splitIntoBytes = splitEvery 3

Even though each pixel can represent many colours we’re really only dealing with black and white here so we can represent each component as fully-on or fully-off. Each pixel can really be stored as boolean values like [True, False, False]. Since it’s possible that some values are not absolutely 0 or absolutely 255 I’ve divided them up the middle — anything darker than 128 is 0, and anything lighter is white.

Once each pixel is a list of booleans we can collapse that down into a single black/white value by taking the conjunction. If all values are True then the pixel is True (ie, black) otherwise False (white).

normalise = and . map (< 128)

At this stage our image is no longer a list of integers but a list of booleans. The original list had height-times-width-times-3 elements. Since we’ve collapsed all those three elements into a single value representing each pixel we now have height-times-width elements. The image is 350x175 pixels so we can split it into rows by cutting the list every 350 elements. This gives us 175 rows.

tomatrix = splitEvery 350 . map normalise . splitIntoBytes

The next stage is, I think, the most beautiful aspect of representing the image as a list of lists. We have a full image but we only want the wavy lines of pixels which make up the border. How do we extract those pixels?

The first thing to notice is that the border is not continuous. The top and bottom edges go to the edge of the screen at both sides, but the two sides don’t meet at the top or bottom. To illustrate:

#################
 
#               #
#               #
#               #
 
#################

So the first question, “where do we start and end?” is answered for us. Each segment is discrete. It was my colleague Rich which pointed out the slight gaps in the border which makes this simplification possible. If the border were complete we’d have to determine whether the corner pieces were part of both the horizontal and the vertical (like a crossword where Across and Down share letters) or not.

The second question we ask is, “which direction does the sequence go in?”. Do we go clockwise from top left, following this alphabetical sequence?

a b c d e
n       f
m       g
l k j i h

Or do we maybe scan left-to-right, ignoring gaps?

a b c d e
f       g
h       i
j k l m n

What about anticlockwise? A mixture of the above? I took the approach which seemed obvious to me, clockwise from top left, and it turned out to be correct. But interestingly the final message is repeated in part so choosing the wrong start point would not have mattered, and it would have been obvious that the output was almost right.

Each row is a list, stored in order from top to bottom. This means the top border is just the first list:

topedge = head

The bottom border is the last list, but because we’ve chosen clockwise we need to reverse the list too.

bottomedge = reverse . last

The right edge is the last element of each list, ignoring the first 3 rows and the last three rows, because as mentioned above, the side patterns are shorter. These two look slightly complicated but it’s mostly dealing with trimming the top and bottom edges off.

rightedge = reverse . drop 3  . reverse . map last . drop 3
leftedge = drop 3 . reverse . map head . drop 3

Now we can extract each edge of the border we can join them all together into our encoded message. This converts our list of lists, which is a complete picture, into a list of bits encoded in the border.

msgstream :: [[Bool]] -> [Bool]
msgstream bits = concatMap ($ bits) [topedge, rightedge, bottomedge, leftedge]

Now we have a long list of bits. And it just so happens the number of bits we have is divisible by eight! This is a good sign because binary information is typically grouped into sets of eight. For the next stage we group our list into sets of 8 bits and turn each 8 into a single number.

One of the tricky aspects about any number is that you can’t tell in advance which end to start from. You and I know that 12 is “twelve” not “twenty-one” but that’s because we know to read numbers from left to right. Computer formats have used both in the past so I wasn’t sure which one would be important to me — is the biggest number the first digit or the last digit? The actual question is, “is the leading digit the most significant bit or the least significant bit?”. I calculated both to see what would happen, and it turned out that most-significant-bit was the way to go. Thankfully, MSB and LSB are just the reverse of each other, so by implementing one we get the other for free!

msb,lsb :: [Bool] -> Int
msb = lsb . reverse
lsb = bitsToInt . map (fromIntegral . fromEnum)

We calculate least significant bit by converting all the True values to 1 and all the False values to zero, and then multiplying element-wise by a stream of powers of two. To illustrate:

  1 2 4 8 16
* 0 1 1 0 1
= 0 2 4 0 16

Then we just add that list up, so “0 1 1 0 1” is “0+2+4+0+16” or 22.

bitsToInt = sum . zipWith (*) (iterate (2*) 1)

After all that prelude we can put this segment together, dividing the image up into its matrix, extracting the bits from the border of the image, splicing them up into sets of eight and converting each 8 bits into a single number:

msgbits = map msb . splitEvery 8 . msgstream . tomatrix

Now what do we do with our numbers? Readable characters are represented internally as numbers, so it is a simple thing to convert between number and printable characters. If we convert each number to a character we get nonsense, but consistent and tantalising nonsense:

Cyrnfr sbyybj guvf yvax: uggcf://plorefrphevglpunyyratr.bet.hx/834wgc.ugzy uggcf://plorefrphevglpunyyratr.bet.hx/834wgc.ugzy

Look at those sequences “uggcf://” repeated twice. That looks so much like a web address, “https://”. If we assume that it is a web address how has it been altered? Each letter in a pair, h/u, t/g, c/p, is 13 characters apart from its partner. But the punctuation symbols aren’t any different.

This looks like the encoding called “rot13” where each character is shifted 13 characters along in the alphabet, and if we reach the end we wrap back to the start. Also, since the first letter of the nonsense message is a capital and none of the rest are it seems like case is being preserved by this encoding.

We convert back to sensible words by rot13 encoding again, since 13+13=26 so any two applications of this transformation will undo each other.

Uppercase and lowercase are treated separately but by the same process. We’re processing some character which we call c and we want to know how many characters it is away from the start of the alphabet. The letter ‘a’ (or ‘A’) is 0 characters away from the start, ‘b’ is 1 character and so on.

If we assume an infinite stream of letters “a b c … x y z a b c…” repeating the alphabet, then the Nth letter in that stream is the one which is N away from the start. The 0th letter is ‘a’, the first letter ‘b’. But if we chop the first 13 characters off this stream, so it’s “n o p … y z a b c …” then the 0th letter is ‘n’, the 1st letter ‘o’ and so on. Each offset now directly maps one letter onto its partner letter. And because the sequences of letters is endless we don’t have to worry about falling off the end. The mapping just loops back on itself:

0 1 2 3 4 5 6 ...
a b c d e f g ...
n o p q r s t ...

Thus we can find the alternate character in our pair by checking first of all how many characters our current letter is from the start, and then looking for the equivalent character in the list which has had its head chopped off. We do the same for the upper case characters and just pass through unchanged anything which isn’t upper or lower case — all the punctuation and spaces.

rot13 :: Char -> Char
rot13 c | isLower c = lowercase!!(ord c - ord 'a')
        | isUpper c = uppercase!!(ord c - ord 'A')
        | otherwise = c
  where lowercase = drop 13 $ cycle ['a'..'z']
        uppercase = map toUpper lowercase

By now I think you’re dying to know what the message says, so let’s finish up here. We decipher a message by converting each integer to a character and performing a rot13 transformation — then we print it.

decipher = putStrLn . map (rot13 . chr)
main = getimage >>= decipher . msgbits

The whole thing is pulled together so we can run it from the command line and we receive the sensible output of:

Please follow this link:
https://cybersecuritychallenge.org.uk/834jtp.html https://cybersecuritychallenge.org.uk/834jtp.html

Next time I’ll look at what happens when we follow that link, and how we complete the next phase of the challenge.

If any of this doesn’t make sense or is confusing please ask questions in the comments. If you want to look at the code in full you can read the solutions for part 1 and part 2 online at http://www.dougalstanton.net/code/cybersecurity/.

As I mentioned in my introductory post I was incredibly impressed by the easy exploratory power of the Haskell code I wrote. Writing little segments to splice, decode, convert and transform made it simple to try out different ways of getting sensible output. I had no idea when I started which way the answer would take me, but putting them together in different combinations in the interpreter was easy and provided instant feedback. (That being said, Rich kinda floored me with his ability to wrangle Excel of all things into solving this problem, though that doesn’t mean it’s the right tool for the job!) Tune in next time for more exciting cryptographic games!

I posted a couple of days ago about one of the earlier exercises (ex1.33) in SICP. After some discussion with Brent Yorgey on Facebook I had another look at some of the definitions given in the book. Yes, if in doubt, re-read the question! :-)

The issue that needed clarified was whether I could justify treating the null-value argument as a full-blown identity element. The text says:

a null-value that specifies what base value to use when the terms run out.

(It’s worth noting that the definition of combiner also isn’t specified very well: a “procedure (of two arguments) that specifies how the current term is to be combined with the accumulation of the preceding terms”.)

This isn’t abundantly clear but it suggests that null-value is the last element that can be included in the calculation, so that:

5 + 4 + 3 + 2 + 1 + 0

is allowed but

0 + 1 + 2 + 3 + 4 + 5

is not allowed, because I’m starting with my null-value (ie, 0) and adding the remaining values to it. In this case there is no difference in result. So I needed to find a situation where some element work as an identity on the right but not on the left. Wikipedia to the rescue!

The number 1 as an identity element for exponents if it’s the power but not if it’s the base. Using ^ as an infix exponent function, for any x:

x ^ 1 = x

but

1 ^ x = 1

We can create a chain of odd-numbered exponents to test our implementations of filter-accumulate:

(define (odd-exponent-chain a b)
  (filtered-accumulate odd? expt 1 identity a inc b))

An implementation of filtered-accumulate which cleaves as closely as possible to the definitions should implement (odd-exponent-chain 2 6) as (expt 3 (expt 5 1)).

This conclusion that null-value only works as a right-identity has further repercussions — most of the answers published for iterative version of accumulate are wrong. Why?

(define (accumulate combiner null-value term a next b) 
  (define (go acc n) 
    (if (> n b)
        acc
        (go (combiner acc (term a)) (next n)))) 
  (go null-value a))

The iterative versions always start with the null-value in the accumulator and slowly combine each new term until the end. But the definition above clearly states that null-value is to be combined with the results when there are no more terms left.

This is possible but not as elegant as the recursive solution by a long shot. There’s probably a good way of cleaning it up that I haven’t spotted yet.

(define (accumulate-iter combiner null-value term a next b)
  (define (go acc n)
    (if (n > b)
        (combiner acc null-value)
        (go (combiner acc (term n)) (next n))))
  (if (a > b)
      null-value
      (go (term a) (next a))))

Having got this far we realise we can no longer implement filtered-accumulate in terms of accumulate: the first term forms the seed for the accumulator whether it is appropriate or not. In this case we do have to create a new filtered-accumulate which is more powerful than accumulate on its own.

(define (filtered-accumulate-iter filter combiner null-value term a next b)
  (define (go acc n)
    (if (n > b)
        (combiner acc null-value)
        (go (combiner acc (term n)) (next n))))
  (define (start n)
    (cond ((n > b) null-value)
          ((filter n) (go (term n) (next n)))
          (else (start (next n)))))
  (start a))

After all this it seems prudent to ask “who’s being pedantic here?” and whether the mistakes identified are the right ones.

• The lack of formal specification of parameters like null-value encourages assumptions. Most people doing these exercises assumed that null-value works as an identity element per the examples of (+,0) and (*,1). These examples reinforced rather than highlighted the assumptions.
• With this assumption it is possible to implement filtered-accumulate in terms of accumulate, contra the question. I haven’t found an instance online where someone spotted this mismatch.
• The “obvious” ways of writing the iterative and recursive accumulate have different semantics if you don’t pay close attention. (Which is another way of saying one of them is wrong.) Hence the problem with making poor assumptions.
• The only way that requires a rewrite of filtered-accumulate is one that doesn’t assume a left-identity element.
• There is an official tutor’s book published but not available online (presumably to prohibit cheating for universities who use this textbook). So we don’t know what the writers had in mind when they wrote that section.

It’s been an interesting few days of thinking! Many thanks to Brent for making me re-examine the text and my assumptions a further time. I think we got to the bottom of it in the end.