Last year Eric Wastl published a set of programming challenges as Advent of Code. I recently went through them, and just made my Python solutions available via GitLab. Feel free to have a look, but please refrain from contacting me with questions about it.

I recently came across an article on ArsTechnica that was the epitome of the inane “More XX chromosome carriers in Tech” propaganda that has been infesting this industry for quite some time. Of course, the problem is not that there should be no women in tech, but that there is a celebration of pseudo-achievements that do the industry, the organizations behind this social engineering initiative, and women themselves a disservice.

In the story, entitled This 11-year-old is selling cryptographically secure passwords for $2 each, we learn that Mira Modi the daughter of Julia Angwin, a “veteran privacy-minded journalist” is selling “cryptographically secure passwords”. As you you read the article, you are tempted to conclude that Mira Modo has simply been paraded around by her mother, as she seems to have little insight into what she is actually doing. In the end, the entire story boils down to her mother looking for a cute marketing gimmick, which made her enlist her daughter for selling passwords on her book tour — and now there is a website, too!

The idea behind Diceware passwords is simple: you roll five dice, or one die five times, and then look up the corresponding word in a publicly available list, which pairs a number combination with a string. For instance, if you throw 5-5-6-5-5, your passphrase is “suave”. One word itself is not particularly secure, since it would yield to a simple dictionary attack. Thus, you should repeat this process a few times, and concatenate all phrases you generate this way. There are 6^5 = 7776 words in the Dicewords list, so feel free to exponentiate this number at will. For instance, after six rounds, you end up with one out of 7776^6 possible combinations.

Overall, following this procedure is trivial. Yet, ArsTechnica found plenty to gush about. Mira Modi is quoted with,

I wanted to make it a public thing because I wasn’t getting very much money,” she said. “I thought it would be fun to have my own website.”

Each time an order comes in, Modi rolls physical dice and looks up the words in a printed copy of the Diceware word list. She writes—by hand—the corresponding password string onto a piece of paper and sends it by postal mail to the customer. (Full disclosure: I ordered two.)

That sounds like an amazing business indeed. In fact, she does not even generate enough money to cover the cost of a domain name and hosting. Considering that she has getting free publicity by her mother, it’s not a very impressive business at all. Yet, this does not keep the fawning journalist from demonstrating to the world his naivety:

If she kept busy at it full-time, Modi would be raking in about $12 per hour—fully one-third more than New York state’s $8.75 minimum wage, which is set to go up to $9.00 on December 31, 2015. As of now, she said she’s sold “around 30” in total, including in-person sales.

Oh, so she barely sells any passwords, but if she suddenly managed to sell more passwords in a day than she sold since starting her business, she would beat minimum wage. Needless to say, if she ever had to hire employees, in case her business enters hockey stick growth, she won’t even break even, assuming labor, materials and shipping aren’t for free. I found the numbers amusing, though, because they suggest that it takes her ten minutes to generate a pass phrase. Guess what also takes about ten minutes? Writing a script that does this for you automatically and which can spew out pass phrases until the cows come home. In very straightforward Python, it looks like this (also on Github):

from random import randint
WORDLIST = "diceware.wordlist.asc.txt"
PARTS = 6
def createPhrase(dct, nums):
result = ""
for i in range(0, nums):
result += dct[throwDice()] + " "
return result
def throwDice():
result = ""
for i in range(0,5):
result += str(randint(1,6))
return result
def main():
with open(WORDLIST, "r") as ins:
diceDict = {}
for line in ins:
(nums, word) = line.split()
diceDict[nums] = word
print createPhrase(diceDict, PARTS)
main()

A clear giveaway that little Mira Modi does not really grasp her business, which was arguably all the creation of her mother anyway is that the ArsTechnica article shows the following picture:

That’s right, a publicly available list is declared “top secret”.

What I find grating about articles like this is that they celebrate non-achievement. It would be far more impressive to find an 11-year old who is able to write a simple program that would automate this task, and if said 11-year old had a well-connected parent, we would surely see articles in ArsTechnica about them as well, which would be just as misplaced because a modicum of precocity is hardly worthy of a story. This ties into a much bigger problem of today’s education at the primary and secondary level. Pupils are coddled, and don’t really learn to exert real effort. But those who continue their education at a decent university and who do not enroll in a fluffy subject will have a rude awakening. After covering Diceware and hinting at the downsides of today’s education, it’s now time to move on to talk about “security theater”.

I mentioned that a computer program would be able to automate the task of generating pass phrases. The Diceware webpage does not agree, but it is mistaken:

Can I use a computer to generate Diceware passphrases?

Generating truly random numbers using a computer is very tricky. The so-called random number generators that come with most programming libraries are nowhere near good enough. For most users dice is by far a better way to select passphrase words.

This is nonsense. To be more polite, it is an example of FUD. True, the randomness in your machine is not truly random. Using a computer program for generating Diceware phrases, though, is safe for precisely the reason that it is simply implausible that an attacker would be able to recreate and maintain the exact same state (!) your machine was in when you ran a Diceware generator. If an entity was as powerful as that, it surely would find more efficient uses for their resources.

FUD seems to be the forte of Arnold G. Reinhold, the creator of Dicewords, as he gives the following advice:

For maximum security make sure you are alone and close the curtains. Write on a hard surface — not on a pad of paper. After you memorize your passphrase, burn your notes, pulverize the ashes and flush them down the toilet.

This would have worked in the world of James Bond in the 1960s. However, today’s super villains of course have cameras installed everywhere, so you better construct the resulting passphrase entirely in your head. Indeed, once you try them on, tinfoil hats are somewhat comfortable. Let’s get back to reality, though. In case you have not been following the news for a couple of years, you should know that privacy on the Internet does not really exist anymore.

Widespread electronic surveillance is commonplace. For instance, the NSA has direct access to Google, Facebook and Apple, as well as others, though their PRISM program anyway. (Here is an article from The Guardian on PRISM.) Thus, they would not need to “hack” your password. Also, there have been several cases of backdoors. So, despite advances in cryptography, it seems that the intelligence agencies of the world would simply sidestep the issues of passwords altogether by getting access to your data in some other way. This does not mean that all your passwords should be “password”, though. Thus, let’s hope that Mira Modi always draws the curtains before generating Diceware pass phrases and does not communicate with her customers electronically.

In early June I submitted the final revision of my Bachelor’s thesis, with the potentially impenetrable title “Compiling Agda to System Fω in Theory”.

I wrote this thesis under the supervision of Andreas Abel (Chalmers University of Technology), who is one of the main Agda implementers.

Abstract:

We develop a theoretical foundation for compiling the programming language Agda to System Fω, which is a stepping stone towards a compiler from Agda to Haskell. The practical relevance for software engineering and the problem of providing correctness guarantees for programs is highlighted. After describing relevant λ-calculi, we specify the semantics for compiling Agda to System Fω. Finally, we illustrate those compilation rules by manually translating several Agda code examples to System Fω.

Unfortunately I’m not able to share most of my university course work, due to our honor code. There are some exceptions, though. For instance, the last assignment in Patrik Jansson’s MSc/PhD course Advanced Functional Programming at Chalmers University of Technology is self-directed and open-ended. The general task is to “read, understand, evaluate and extend an advanced Haskell code base”, with the underlying goal of getting us students involved with an ongoing local research project, or in open-source development by contributing to one of the more popular Haskell package on Hackage.

In this article I will merely provide some background for the work we did, including relevant references. The information below should suffice to give an overview of this project.

Emil Axelsson, one of the authors of the Feldspar language [1], which is an embedded DSL for digital signal processing that is implemented in Haskell, gave a guest lecture on combining deep and shallow embeddings [2], and how this technique was used for the implementation of Feldspar.

In our project, my lab partner Niklas Logren and me collaborated with Markus Aronsson, a PhD Student in the Software Technology division in the Department of Computer Science and Engineering at Chalmers. Markus is currently working on a synchronous data flow extension to Feldspar, i.e. an extension to Feldspar that allows it to operate on streams. For details, please refer to the corresponding paper [3].

We implemented an FFT based on Cooley-Tukey. Our implementation is based on the FFT implementation that is outlined by Bjesse, Claessen and Sheeran in their paper on the hardware description language Lava [4]. Our entire code is available in my Github repository gregorulm/fft_feldspar. Markus Aronsson’s Feldspar extension is currently work-in-progress and not publicly available. Our FFT implementation, though, will be part of the eventual release.

References:

[1] E. Axelsson, K. Claessen, G. Devai, Z. Horvath, K. Keijzer, B. Lyckegard, A. Persson, M. Sheeran, J. Svenningsson, and A. Vajda. “Feldspar: A domain specific language for digital signal processing algorithms”. MEMOCODE 2010.

[2] J. Svenningsson and E. Axelsson. “Combining deep and shallow embedding for EDSL”. Trends in Functional Programming, LLNCS 2012.

[3] M. Aronsson, E. Axelsson, M. Sheeran. “Stream Processing for Embedded Domain Specific Languages”, (draft, submitted to IFL 2014).

[4] P. Bjesse, K. Claessen, M. Sheeran, S. Singh. “Lava: Hardware design in Haskell”, International Conference on Functional Programming, pp. 174–184, 1998.

In Bove and Dybjer’s Agda tutorial “Dependent Types at Work”, section 2.5 briefly introduces Gödel’s System T, which is based on the simply typed lambda calculus with booleans and natural numbers. They give Agda definitions of the primitives of System T, as well as the multiplication and addition operator, using those primitives. As an exercise to the reader, they ask for for further definitions like cut-off subtraction and a few Boolean operations.

Building abstractions by using this rather limited set of primitives turned out to be a pleasant diversion, so I went on and implemented further operations. But to start, here are the primitives of System T in Agda, as they were given by the authors. The six primitives of System T are true, false, zero, succ, if_then_else_, and natrec, i.e. recursion on natural numbers.

module SystemT where
data Bool : Set where
true : Bool
false : Bool
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
if_then_else_ : {C : Set} → Bool → C → C → C
if true then x else y = x
if false then x else y = y
natrec : {C : Set} → C → (ℕ → C → C) → ℕ → C
natrec p h zero = p
natrec p h (succ n) = h n (natrec p h n)

Further, Bove and Dybjer give definitions for addition and multiplication:

_+_ : ℕ → ℕ → ℕ
_+_ n m = natrec m (λ x y → succ y) n
_*_ : ℕ → ℕ → ℕ
_*_ n m = natrec zero (λ x y → y + m) n

The subtraction operation requires the predecessor function. Note that the predecessor of zero is zero. Further note that since we are restricting ourselves to natural numbers, subtraction is defined as so-called cut-off subtraction. This means that computations that yield negative numbers when performed on integers yield zero instead. Concretely, 1 – 2 = 0 instead of -1 because we restrict ourselves to nonnegative integers.

pred : ℕ → ℕ
pred n = natrec n (λ x y → x) n
_-_ : ℕ → ℕ → ℕ
_-_ n m = natrec n (λ x y → (pred y)) m

This might look a bit hairy, so it’s probably helpful to walk through this function. First, subtract one from zero:

zero - (succ zero)
= natrec zero (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec zero (λ x y → pred y) zero)
= (λ x y → pred y) zero zero
= pred zero
= zero

Second, two minus one:

(succ (succ zero)) - (succ zero)
= natrec (succ (succ zero)) (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec (succ (succ zero)) (λ x y → pred y) zero)
= (λ x y → pred y) zero (succ (succ zero))
= pred (succ (succ zero))
= succ zero

To do a bit more in System T, Boolean operators would be nice to have. Using “if_then_else_” the operators for not, and, or, and xor are straightforward to define:

¬ : Bool → Bool
¬ b = if b then false else true
_∧_ : Bool → Bool → Bool
a ∧ b = if a then b else false
_∨_ : Bool → Bool → Bool
a ∨ b = if a then true else b
_⊕_ : Bool → Bool → Bool
a ⊕ b = if a then (¬ b) else b

An equality check for boolean values follows naturally:

equalityBool : Bool → Bool → Bool
equalityBool a b = if a then (a ∧ b) else (¬ (a ∧ b))

On the other hand, I found the definition of equality for natural numbers tricky. The function ‘zero?’ is therefore not defined using the perviously mentioned primitives of System T. I’ll have to look further into lambda calculus. As it is, ‘zero?’ is a small blemish of this implementation of System T.

zero? : ℕ → Bool
zero? zero = true
zero? _ = false
positive? : ℕ → Bool
positive? n = ¬ (zero? n) -- there are no negative numbers
equalityNat : ℕ → ℕ → Bool
equalityNat a b = (zero? (a - b)) ∧ (zero? (b - a))

Lastly, here are comparison operators for natural numbers:

_>_ : ℕ → ℕ → Bool
a > b = positive? (a - b)
_<_ : ℕ → ℕ → Bool
a < b = positive? (b - a)
_≥_ : ℕ → ℕ → Bool
a ≥ b = (a > b) ∨ (equalityNat a b)
_≤_ : ℕ → ℕ → Bool
a ≤ b = (a < b) ∨ (equalityNat a b)

All of this looks pretty clean. I let Agda evaluate a few expressions, which all worked fine.