benc technical blog

2012-01-28T02:30:00.000Z

Well, I came across a magic line of HTML for making a website look basically readable on an iPhone. Not magic in the sense that I don't understand what it does. But magic in the sense that its a single line that is the first big step to making a site look OK.

The line is (to go in your <head> section:
<meta name="viewport" content="width = device-width" />

What it does is make the iPhone web browser render the HTML at a sensible readable font size, with word wrapping at the end of the screen. (the default, otherwise, is to try to fit a regular screen worth of pixels across, then zoom out to make it fit on the small iPhone screen - that means the user has to zoom and pan to do anything).

Now my pages still look like crappy hand written HTML, but at least they're readable on an iPhone now.

I added this to the shellinabox installation I have on barwen.ch, and now its much prettier to use a browser-based shell on an iphone - you get a 30 character terminal thats at sensible font size, rather than a wide wide terminal at unreadable font size.

Two hardware OTP keys

2012-01-21T10:18:00.000Z

I got a couple of OTP (one time password) keys to try out. These are hardware dongles that generate a unique code number every time you use them, which you then use in addition to a password when you log in to places (eg your server, some website).

The goal is to make things more secure by not having a password someone can steal.

The mechanics of this used to be hard to describe but enough people use online banking with security tokens now (at least in western europe) that the idea is pretty widely known already. (You can read about two factor authentication on wikipedia)

First, I tried a yubikey. Yubikey comes with a silly tagline, "the key to the cloud", but don't let that put you off. The yubikey plugs into a USB port on your computer and when you press its single button, it types in the next code in sequence as if it was a USB keyboard. I've tried this on a linux box and and an OS X box and it had no problem on either.

Pressing a button seems much less hassle than typing in a code off an LCD screen, but it does come with downsides: you need to have the device in a USB slot when you press the button. On a tower desktop, that's possibly down by the floor. Even worse, maybe you don't have a USB slot at all, in which case the device is useless.

yubikey has a number of different modes, and can store two configurations at once (yes, even though it has just one button).

There's a yubikey proprietary mode which generates a long key string which contains a bunch of stuff (for example, a device ID); an HOTP mode which generates a 6 or 8 character code (with programmable extra decoration); and a static mode which types in a preprogrammed fixed 64 character string. This is all configured by some software that you get for free off the yubikey website. I'm always a bit wary of vendor software to support hardware devices, because it often seems a much lower priority than the hardware device itself. But this worked well enough.

I only tried out the HOTP mode, because I wanted interoperability with other OTP implementations.

The two configurations are accessed by holding down the button either for less than 2s or for more than 2s. I've only used the first configuration, and I haven't had any trouble with accidentally falling through to the second one. But it sounds a bit cracked out and if I was giving it to the kind of user who would hold the button extra long "just to be sure," then maybe there would be trouble. I was hoping there would be an option to switch that second configuration off, but I didn't see one.

My only interaction with the supplier, yubico, was to order the key online, for $30+VAT. This arrived 24h after I order it, by regular mail (from the next village over!).

The second device I got was an OTP C200 token from Gooze. This has a more traditional user interface with a 6 digit LCD display and a button which turns on/off the display. The C200 is a TOTP token: HOTP, except the code changes every 30 seconds instead of when you press the button.

Gooze also makes a C100 which is regular HOTP. I haven't tried one of these, but the design of the C200 case makes me think that the button would get pressed a bunch randomly if you're carrying this with your keys in your pocket. With TOTP, that's not a problem - the code is not related to the button press. But I've encountered loss-of-sync troubles with other hardware tokens before due to this and I don't think the C100 solves that problem.

There is no configuration of the device itself needed - it only does TOTP, and the seed value is preloaded. You get sent that by Gooze. This was sent by GPG encrypted mail so I could cut and paste it into the configuration of my server easily. It means Gooze knows your secret key (although they claim to delete them after sending). I'm not too fussed by that because I'm not aiming for über-high security, but I'm sure some people will.

Worse though was that through some mess up in customer service, it took them over a week to get the codes to me after the devices arrived, and they were pretty silent during that week despite repeated enquiries. I think this is due to the company being pretty small. This is almost enough to make me not order from them again.

Because the C200 has a screen, you have to read the code and type it into your computer by hand. So some properties are inverted from the yubikey: it's a hassle to type in the code; but it doesn't matter if you have a USB port. Because of that, I think this is more appropriate than the yubikey for "I'm going on holiday but want to be able to access my email from public terminals" uses.

I wired both of these up to pam_oath to log into my linux servers; maybe I'll write about that side of things another time. Neither device has beaten the other in being my favourite - the yubikey has substantially higher geek value for plugging into a USB port and greater convenience in some circumstances, but the C200 feels more practical for other use cases such as connecting from unfamilar devices. I've only had a few days to form the above opinions and I expect I'll form more opinions over time.

server availability like uptime

2012-01-15T19:28:00.000Z

I wondered if I could get a measure of server availability as a single number, automatically (for calculating things like how tragically few nines of uptime my own servers have)

So, I wrote a tool called long-uptime which you use like this:

The first time you run the code, initialise the counter. You can specify your estimate, or let it default to 0:


$ long-uptime --init

and then every minute in a cronjob run this:


$ long-uptime
0.8974271427587808

which means that the site has 89.7% uptime.

It computes an exponentially weighted average with a decay constant (which is a bit like a half life) of a month. This is how unix load averages (the last three values that come out of the uptime command) are calculated, though with much shorter decay constants of 1, 5, and 15 minutes.

When the machine is up (that is, you are running long-uptime in a cron job), then the average moves towards 1. When the machine is down (that is, you are not running long-uptime), then the average moves towards 0. Or rather, the first time you run long-uptime after a break, it realises you haven't run it during the downtime and recomputes the average as if it had been accumulating 0 scores.

Download the code:


$ wget http://www.hawaga.org.uk/tmp/long-uptime-0.1.tar.gz
$ tar xzvf long-uptime-0.1.tar.gz
$ cabal install
$ long-uptime --init

cuba

2012-01-09T12:42:00.002Z

was in cuba for a month. internet is hard there (though possible) so no updates on this blog in that time. sorry.

https in cpanel

2011-12-10T11:38:00.000Z

working with someone who has a cpanel server. they want https on it. cpanel doesn't do that by default. google doesn't reveal much in the way of tutorials for this, so here's a note for people to find.

generate a key pair and certificate using theGenerate a SSL Certificate & Signing Request page. Copy the certificate onto your clipboard.
go to the Install a SSL Certificate and Setup the Domain page. Paste in the certificate. click fetch on the key text field and it should populate that field for you. Set the username to nobody so that all users can use this key pair.
When you save that page, apache will reload and you'll get https service on port 443, with a self-signed certificate (and so with consequent certificate mismatch error messages). But your existing domains won't work on that server - they'll go to the default cpanel parking page - cpanel only configures its virtual hosts on port 80... grr
So next I made an apache mod_rewrite rule in the VirtualHost directive for the port 443 virtual server. That causes all the internal sites appear on port 443.
```
    RewriteEngine on
    RewriteRule   ^(.+)          http://%{HTTP_HOST}$1 [P]
```
That's an awkward hack to have to add to cpanel's generated config, but it seems to work (modulo invalid certificate warnings that all users ignore anyway)...

There's also a hole in the way that that rewrite rule is implemented: with a custom http client, you can probably make this server act as an arbitrary proxy for you, depending on mod_proxy configuration.

DHmPC

2011-12-03T15:01:00.002Z

I have a server running inside EC2. It gets its network details using dhcp.

ubuntu@s0:~$ hostname
s0.barwen.ch
ubuntu@s0:~$ hostname --fqdn
hostname: Name or service not known

grr.

This happens pretty much every time the VM reboots. Its something to do with getting a new private IP address each time it reboots.

Although this manages to work:

hostname --all-fqdns
s0.barwen.ch polm.pl stacheldraht.it s0.barwen.ch

The autoconfigured resolv.conf looks like this:

nameserver 172.16.0.23
domain eu-west-1.compute.internal
search eu-west-1.compute.internal

and if I comment out or remove both the domain and search lines, then everything works...

Those lines are wrong anyway - this machine is in my barwen.ch domain. It just happens to be hosted in amazon's network...

mysql rsync backup doh!

2011-11-29T12:24:00.002Z

Well, I moved a big live database from one server to another for a customer. I was planning on taking the site offline first and doing an sql dump/move/restore, but someone accidentally deleted the old server before they were meant too (oops) - leaving me with some rsync backups that I'd made of the whole server over the previous days, to guard against such an eventuality.

Turns out rsyncing a live mysql database is not the right way to do things - I ended up with a database that managed to get mysqld to actually crash when I tried to dump out the database contents. I managed to fix this by dropping the tables that it was crashing on: it conveniently told me which ones it was crashing on, and it let me drop them, just not dump them. Luckily they were all cache tables so there didn't seem to be harm in dropping them and recreating them empty.

It also turns out (obviously, post facto) that mysql databases don't play nicely with rsync's --link-dest option, which is supposed to reduce disk space on the target file system when making multiple snapshots. Because it only optimises away duplicate data for identical files, but mysql stores the entire database (to a first approximation) in a single file, hiding its internal structure from rsync, and so the whole db gets duplicated each time.

Taking an SQL dump should solve the first problem. Not entirely sure what the right way to do an incremental backup of the database is. Maybe I shouldn't even try.

batch checking DNS delegation

2011-11-19T08:26:00.001Z

I'm working with someone who has ten or so domains. All the domains are registered in different places, and with slightly different DNS settings. As part of tidying that up to get everything consistent, I wrote the following bash+dig script to display the delegation of each zone from its parent.

That is importantly not the same as what the name servers for the zone return as NS records. The "authoritative" source of NS (nameserver) records for a zone is that zone itself. Using dig to query the NS records seems to be returning those, unsurprisingly.

However, in order to query a zone, there is a second place where name servers must be configured, separately from in the zone itself. That is in the parent zone. If those are wrong, then you can get awkward to diagnose problems: you can see from dig that the nameservers are right, yet lookups go to the wrong place.

Hence my script.

You can see even on my own domains there's a slight misconfiguration: barwen.ch claims to have s0.barwen.ch as a server, but the .ch registry isn't delegating to it. That won't cause bad DNS lookups but will cause s0.barwen.ch to not be used as a nameserver sometimes. Worse is when the delegation points to an old server that then returns a new servers DNS, giving the illusion that all is well, until you turn off the old server (which is the problem I have on other zones)


$ ./list-domains-NS.sh 
ZONE hawaga.org.uk
NAMESERVERS ACCORDING TO GOOGLE DNS
dildano.hawaga.org.uk.
paella.hawaga.org.uk.
NAMESERVERS ACCORDING TO org.uk
hawaga.org.uk.  172800 IN NS paella.hawaga.org.uk.
hawaga.org.uk.  172800 IN NS dildano.hawaga.org.uk.

ZONE barwen.ch
NAMESERVERS ACCORDING TO GOOGLE DNS
paella.hawaga.org.uk.
s0.barwen.ch.
dildano.hawaga.org.uk.
NAMESERVERS ACCORDING TO ch
barwen.ch.  3600 IN NS dildano.hawaga.org.uk.
barwen.ch.  3600 IN NS paella.hawaga.org.uk.

So here's the script:


#!/bin/bash
cat domainlist.txt | while read d ; do
  echo "ZONE $d"
  echo "NAMESERVERS ACCORDING TO GOOGLE DNS"
  dig @8.8.8.8 -t ns $d +short

  PARENT=$(echo $d | sed 's/^[^.]*\.//')
  echo "NAMESERVERS ACCORDING TO $PARENT"

  PARENTNS=$(dig +short -t NS ${PARENT}. | head -n 1)

  dig @$PARENTNS -t NS +noall +authority +norecurse $d

  echo
done

country selector

2011-11-12T11:06:00.008Z

I've had a rant queued up on this blog but never completed about various forms of internationalisation/localisation.

One part of the rant is about web forms that ask for your country. A common way to do this is a drop down list of "every country" (deliberately in quotes). That's awful.

Its especially awful when you are from simultaneously from: Britain; United Kingdom; Great Britain; and England, all "countries" in someone's definition or another - not only do you have to scroll down to your country, you don't even know which of the four countries you are meant to scroll to until you get there and find that country missing.

I saw (on hacker news) this redesigned country selector: http://baymard.com/labs/country-selector which presents an autocompleting text box.

Type "eng" and it brings up "United Kingdom". woo!

It also converts "deut" into "Germany", but fails to convert ”日” into Japan.

beep is not useful.

2011-10-08T10:32:00.000+01:00

sometimes I get a beep on my laptop.my console has ~10 applications on 9 desktops, including being remotely connected to ~5 machines.a beep without any context is not useful.

POSSIBLE BREAK-IN ATTEMPT (not really)

2011-10-01T10:53:00.000+01:00

SSH gives out error messages like this:


Sep 28 09:50:09 s0 sshd[27967]: reverse mapping checking 
                  getaddrinfo for adsl86-34-217-144.romtelecom.net 
                  [86.34.217.144] failed - POSSIBLE BREAK-IN ATTEMPT!

Why does it label it as POSSIBLE BREAK-IN ATTEMPT!?How is it more of a possible break-in attempt than a user attempting to connect more than a few times with a wrong password?This has bugged me a bit recently when helping a few people who aren't really used to linux - its shouting at them that something is SERIOUSLY WRONG!!! and when they look through their log files, they've fixated on this (as far as I can) relatively minor misconfiguration of a remote user's network.

♫ if i could turn back time ♪

2011-09-24T18:57:00.000+01:00

Cooker has a one-way-only knob for setting time. You wind forwards until you reach now. If you miss now, you wind forwards another 24h (luckily the cooker doesn't have a date too) until you reach now again. On TZ shift (i.e. end/start of summertime / daylight savings), once per year, there's a wind-forward 1h event. fairly easy. you make the clock run faster than real time. but once per year there's a once per year wind-forward 23h event. BUT! Turns out if you can stop the clock, then you can let real time wind forwards faster than clock time. and wait an hour. and then start the clock again. It involves more real time (you have to wait an hour) but a lot less tedious winding.

wikipedia find-of-the-day: electronic calculator abacus

2011-09-17T13:35:00.000+01:00

linked on the wikipedia page for Soroban

5 centuries ago...

2011-09-10T16:59:00.000+01:00

I just queued up jobs for a physics simulation that are 5 compute-centuries long:

6 jobs x 11.5 hours x 16384 nodes x 4 cores/node = 5.16 centuries.

I'm expecting the runs to be finished in about a week

If this ran on a single core and I wanted it to be finishing in about a week, I would have had to start them in the year 1495 (the most interesting wikipedia note for that year is Friar John Cor records the first known batch of Scotch whisky).

frustrated-with-slow-simulation haiku

2011-09-03T13:48:00.000+01:00

microseconds pass
simulation time stretched
long as winters night

I can't complain too much though - this was 65536 cores on an IBM BlueGene/P

today is blog day

2011-08-31T01:01:00.000+01:00

Today is blog day (well, today isn't, it's the 19th of May, but hurrah for autopost)

I'm supposed to recommend 5 blogs to you.

I'm also supposed to find *new* blogs. But FTS, I'm too lazy. Plus I know the ones listed here are ones that I know I go back to day after day and find useful.

Oglaf is some dude's NSFW comic that started out as an attempt at cartoon porn but now is mostly funny. The shield maiden is my favourite post.

Hacker News from ycombinator - kinda like slashdot in that its a lot of interesting geek links. More links. Less discussion. Feels more intimate, and more focused around the bay area startup crowd.

Lambda the ultimate - a programming languages weblog. A cross between programming and maths. If you like Haskell, you'll like this, though all sorts of language stuff (theory, design) is talked about. You can also laugh at the "amusing" paper titles that authors come up with.

In a bit of shameless self promotion, I'll point you at the drupal news feed for my hobby project, barwen.ch - this is partly blog, partly just a web page change tracker.

Finally, Bruce Schneier's security blog. Aside from his tendency to ramble on about squids, this is pretty interesting. It evolved out of his company newsletter, and talks mostly about computer security but also about other related topics such as social engineering and terrorism. And squid.

Exbibyte divergence.

2011-08-27T22:38:00.000+01:00

Mostly used by debian crackheads, but slowly becoming more widespread (and apparently also defined by the IEC) is the use of kibibyte to mean a kilobyte measured as 1024 bytes, so that KB can be used to mean kilobyte measured as 1000 bytes. There's a 2.4% difference between the two.

Correspondingly there is Mibibyte, Gibibyte, tebibyte, pebibyte, exbibyte, zebibyte, and yobibyte.

While the difference is only 2.4% at the kibibyte scale, it gets bigger with larger prefixes: by the time you get to petabytes, the scale of the largest file systems I have access to these days, the difference is over 12% and by yobibytes its 20%

brazen sms charging

2011-08-20T12:20:00.000+01:00

Its fairly obvious for anyone who thinks about it for a while that SMS is appalling bad value per-byte compared to IP or voice over the same system.

But Orange UK really made me laugh/cry with the brazen way in which they juxtaposed two menu options to make it so clear:

To buy 50 UK SMSes valid for a day for 1 pound, press 1.
 To buy 50 Mb of data valid for a day for 1 pound, press 2.

Yes, 1 UK SMS == 1 Mb of internet data.

W
T
F

y2.1k bug

2011-08-13T12:22:00.001+01:00

a decade into this century, and I see plenty of people using 2 digit years. we all know where that's leading...

auctions in course allocation

2011-08-06T18:44:00.000+01:00

Apparently some universities use an auction mechanism for allocation of places in courses, as detailed for example in page three of this memo from NYU.

Very briefly describing this in quotes:

Students will be allotted bidding points
After an auction is run, students admitted to a class will be charged a “clearing price” in points equal to the highest bid from a student not admitted to the class at that auction.

HTML Slidy

2011-07-30T09:03:00.002+01:00

HTML Slidy is a neat style sheet for making powerpoint-like presentations that are: i) written in HTML, and ii) appear in a browser. I've used it for one presentation and quite liked it. My presentation was entirely text. I can imagine it being more awkward for graphics-intensive presentations where the automatic reflowing of content to fit the current window turns into a downside rather than an upside.

dnssec revisited

2011-07-23T20:52:00.003+01:00

well I was pleased that my dnssec notes remained sufficiently intelligble after a few months to set up a new zone. but the machine I was just using took almost 5h to generate keys for a new zone. oh the entropy.

browserid in-browser shell logins

2011-07-16T19:10:00.006+01:00

I've previously wired up my shell server barwen.ch to allow browser-based logins using OpenID and shellinabox. I've written about that on this blog before. I saw a few articles about Mozilla's BrowserID. The code snippets there looked like they would integrate well with the code I had already. So my evening project (which ended up only taking about half an hour) was to prototype BrowserID-based shell login.

It works basically the same as for the OpenID login on barwen.ch:

To get set up: you need to sign up for a barwen.ch account which will cost you 50 cents on PayPal; you need to send me the email that you use for BrowserID (instead of / in addition to an SSH key).

To actually log in, go to the login page http://s0.barwen.ch/~benc/browserid.html and log in. A terminal will appear in your browser. You do shell stuff.

This code is pretty crappy so I don't really want to release it until I've had a thought about the security for at least an hour (though you can find fragments of it elsewhere on this blog). I especially think that there might be some attacks possible by using freaky email addresses vs my unsanitised string handling. (I'm looking at you, Bobby Tables).

bbc 500

2011-07-16T16:09:00.000+01:00

During the wedding of the Duke and Duchess of Cambridge in April, the BBC website was for a while overwhelmed and giving http 500 errors. I was amused by the graphic they presented:

which UK viewers above a certain age will find familiar.

blue traffic light

2011-07-09T09:44:00.000+01:00

when I was a little boy, it always struck me that traffic lights should have a blue light in addition to the red and the green (and the amber), though I could never decide what it should be for.

anyway I discovered that in Hong Kong, the MTR East Rail line *does* have a blue light on its signals, so my childhood desire is finally satisfied. it even seems a sensible use:

Passenger trains have been running under an overlaid Automatic Train Protection (ATP) system since 1998. A blue aspect is displayed at signals when a train fitted with working ATP is approaching. A signal showing a blue aspect can be ignored by the driver, who will drive according to the information shown on the cab display.

mrtg user counts

2011-07-02T11:22:00.006+01:00

I had a graph in mrtg of two variables: number of login sessions (the blue line, the count of users from the unix users command), and number of unique users logged in (the green solid area - formed by deduping the output of users).

I decided that the number of login sessions was a bit useless especially with people using screen. A more interesting graph is perhaps something else based on the number of users doing things rather than the number of things a user is doing. So I chose to count the number of (normal, not system) users who have at least one process running.

I count it this way:

#!/bin/bash

# first, unique users logged in
echo $(users | sed 's/ /\n/g' | sort | uniq | wc -l)

# number of users who have 3xxx user numbers and have a process running 
# 3xxx is the "normal user" range, though perhaps I could distinguish in other ways
U=$(ps -A --format user= | sort | uniq | while read a ; do id -u $a ; done | grep -e '3...' | wc -l)

echo $U
echo 0
echo 0

and here's the output: (green is logged-in users, blue is users with processes running)

If you click through to the full page, you might see the change happening in the middle of week 17 of 2011, which is the beginning of May.

non-cidr netmask: "worked in testing but broke colleagues' brains"

2011-06-24T09:59:00.000+01:00

CIDR prefix length (for example, the 24 in 128.9.128.0/24 is a more concise notation for (a commonly used subset of) netmasks.

A prefix length contains less information - it can only represent netmasks that consist of a sequence of 1 bits, followed by 0 bits to the end. For example, /24 is 11111111111111111111111100000000 (24 1s and then 32-24=8 0s)

This is useful because thats how most people use netmasks.

But there's a set of netmasks that aren't representable this way - for example 11111111000000001111111100000000.

Did anyone ever use netmasks that weren't prefix-length-representable? Apparently yes:

Addresses were allocated from these networks sequentially, and the oldest
web sites tended to get the most traffic, so a straightforward setup that
spread the six /18s across the reverse proxies didn't balance the load
particularly well. I toyed with using 0xffff0003 netmasks to split the /16
so that successive addresses could be routed to each of the four London
reverse proxies in turn.

This worked in testing but I didn't deploy it because it broke my
colleagues' brains and non-contiguous netmasks were an unsupported
feature.

password policy for ssh key hosts

2011-06-18T11:24:00.000+01:00

I have a host with a handful of users. When they authenticate, they have to use either ssh public key or openid - there is no on-machine password. But some of the services that are running pretty much need a password: for example, IMAP, SMTP AUTH, web portal.

I'd like to give these users the ability to acquire a password.

Two ways are immediately apparent:

Implement a mechanism which presents the user with a new machine-generated password, for example to their registered email address.
Allow the user to run passwd in a shell, but not require them to enter their existing password first (instead, rely on the fact that they are logged in to be sufficient authentication).

Dear Reader, can you think of other ways? Do you have any opinions on the wiseness/unwiseness of these approaches?

roman numeral literals using Template Haskell

2011-06-10T15:37:00.002+01:00

I've know about Template Haskell (TH) for ages but never used it. As a diversion from another project, I thought I'd try to implement roman numeral literals for Haskell, using TH -- this seems an easy way to get started without having to dig in too far.

I already wrote some Haskell roman numeral code which gives a function numeralsToInteger :: String -> Integer. I tweaked its source code a bit (it wasn't a module previously, for example) and can write this:

import Roman

main = do
  putStrLn "roman test 1 (this should print 1998 below)"
  print $ numeralsToInteger "MCMXCVIII"

What I want to do with TH is shorten the syntax and make the roman->literal conversion happen at compile time instead of at runtime.

I'll try to use TH's quasi-quoter syntax, which should allow me to write:

print [ro|MCMXCVIII|]

ro is the name I've chosen for my quasiquoter, and the [...|...|] bracket syntax comes from template haskell quasiquoting.

What will happen is that everything inside those [|brackets|] will be passed to my code, which can return an arbitrary Haskell expression to be substituted at compile time. Think C-style #define on steroids.

In my case, I'll always be returning an integer literal expression. The value of that literal will be determined by parsing the roman numeral.

I need to define ro :: Language.Haskell.TH.Quote.QuasiQuoter, and it needs to live in a different module (so that it can be compiled before attempting to parse anything that uses that quasiquoter)

I want to use my quasiquoter to return an expression. They can be used in more contexts than that (for example, when a type is needed). I'll make the other contexts into an error, which leaves only the hard one that parses and returns my expression. (after doing a bunch of fiddling Agda, it feels like a relief to be able to say "oh, I'll just make that an error).

It turns out that the code is mostly plumbing. RomanTH.hs looks like this:

module RomanTH where

import Roman
import Language.Haskell.TH
import Language.Haskell.TH.Quote

ro :: Language.Haskell.TH.Quote.QuasiQuoter
ro = QuasiQuoter parser err err err

err = error "Roman numeral quasiquoter cannot be used in this context"

parser :: String -> Q Exp
parser s = litE (IntegerL (numeralsToInteger s))

which is all types and wiring except the functionparser s = litE (IntegerL (numeralsToInteger s)) which means (right-to-left) convert string to an Integer, embed it in a literal type, and embed that inside an expression.

The complete test program looks like this:

import RomanTH

main = do
  putStrLn "roman test 2 (this should print 1998 below)"
  print [ro|MCMXCVIII|]

and runs like this:

$ ./test2 
roman test 2 (this should print 1998 below)
1998

Well, that took all of 36 minutes.

best ipv6 address seen so far

2011-06-08T08:29:00.002+01:00

2600::

It even works, serving http for sprint.net

June 8th is world IPv6 day!

2011-06-08T00:01:00.001+01:00

June 8th is ISOC's "world ipv6 day". According to the organisers:

On 8 June, 2011, Google, Facebook, Yahoo!, Akamai and Limelight Networks will be amongst some of the major organisations that will offer their content over IPv6 for a 24-hour “test flight”. The goal of the Test Flight Day is to motivate organizations across the industry – Internet service providers, hardware makers, operating system vendors and web companies – to prepare their services for IPv6 to ensure a successful transition as IPv4 addresses run out.

Some of us have been trying to do that for years ;)

Anyway, some things you can do:

Read all the ipv6 related posts on this blog
Make sure you are using IPv6 certified cable
Play loops of zen, an ipv6-only browser tile-puzzle
If your ISP does not provide IPv6 and you want easy IPv6 access for a single workstation, I recommend the teredo protocol (its built into windows, and you can apt-get miredo on debian. For a server or network installation, take a look at Hurricane Electric's tunnel broker which will give you a /48 prefix routed over your normal internet connection.
If you're on ipv6 already and you're feeling hardcore you can use NAT64 and DNS64 to get rid of all your local ipv4 traffic, instead routing it all through a NAT gateway at (for example) Andrews and Arnold.

Panickers guide to world ipv6 day

2011-05-29T17:06:00.004+01:00

8th June 2011 is World IPv6 day. Maybe you haven't done anything about getting your website ipv6 enabled. Its taken the world 15 years to develop IPv6, so sure it seems *totally* reasonable that you can get it deployed in 10 days.

What I'm going to tell you about here will get basic IPv6 access to your site. It won't do it in a particularly pretty way, and its probably not the long term way to do it. Also I just hammered this out this afternoon (though its based on years of IPv6 use). (I hope) it should work.

First some DOs and DONTs:

* DON'T deploy IPv6 on your production servers. If you don't know much about IPv6, then blindly sticking it on your real production resources is probably a good way to put even your IPv4 (read: the real IP that everyone actually uses) connectivity at risk (for various reasons that you'll understand when you understand...)

* DO deploy a http proxy server on its own machine, and have that proxy your IPv6 traffic. You shouldn't need to modify *anything* on your production machines.

* DON'T put the IPv6 address record (AAAA, as opposed to the IPv4 A record) in your normal DNS. If you do, then users who have both IPv4 and IPv6 will usually try to connect over IPv6. You don't know how well this is going to scale, or how good your IPv6 connectivity is going to be (or even how good your users ipv6 connectivity is going to be, if everyone is going to be fucking around that day)

* DO put a DNS name (eg www.6.example.com, if your main site is on www.example.com) with the AAAA record. That way, users can choose to try using IPv6, and if its broken can easily get back to your main site. You'll need to publicise this, though, because its not going to get users connecting via IPv6 automatically, and at the same time you should provide some feedback: for example, an email address or a forum.

So what do you need to do:

* Get a dedicated server (either a physical hardware server, or a VPS) running a recent version of Linux. (Ubuntu 10.x would be enough)

* Connect that server to the ipv6 internet. If its on a network with native IPv6, then your host will probably give you connection details. If not, then use Hurricane Electric's free tunnel broker which will connect you over a regular internet connection.

* However you connect, you'll end up with an IPv6 address for your machine. It will be a string something like this 2001:470:1f09:1288::2 that you can get out of ifconfig(specifically, if you have a choice, choose the one that begins with a 2, not the one that begins with an f). Put that IPv6 address into an AAAA record in DNS (better hope your DNS hosting provider does AAAA records - the good ones do...) under a new DNS name. Don't put IPv4 addresses in there too. In my example, I'm going to configure:
blog.6.hawaga.org.uk AAAA 2001:470:1f09:1288::2

* Put apache httpd on your server, apt-get install apache2

* Now you'll need a client machine with IPv6 to try connecting to your new server. If you have a windows PC, you can probably turn on Teredo in the network configuration - it comes built in. On OS X, Linux or BSD, you can install miredo which is a Teredo client. Or you can set up another Hurricane Electric tunnel for your client machine. You can use test-ipv6.com to get a score for how well your new client machine is connected to the ipv6 internet.

* You should now be able to use a web browser to reach the hostname you configured in DNS back there - you should see apache's welcome/default page.

* Now, configure apache to forward all requests it receives onwards to your production website over IPv4. In the following example, my production IPv4 website is the one you are reading right now, benctechnicalblog.blogspot.com. Enable mod_proxy and mod_proxy_http, and then set up a virtual host directive like this (or put it in the base of your server config, seeing as this a host dedicated to forwarding ipv6 traffic):

<virtualHost *:80>
  ServerName blog.6.hawaga.org.uk
  ProxyPass / http://benctechnicalblog.blogspot.com/
  <Proxy http://benctechnicalblog.blogspot.com/>
    Allow from All
  </Proxy>
</virtualhost>

Once you've done that, visiting your ipv6 hostname (eg blog.6.hawaga.org.uk) should serve you the content of your real production website website.

Now publish the new hostname in a news item and make it seem like you know what you're doing...

Some stuff will not work, for sure: if you have anything that does things based on IPv4 address of client, that's all going to be based on the address of the proxy machine, not the real client IPv6 address. Things that might affect are localisation (eg language), and rate/load limiting based on ip address.

So, please ask questions in the comments and I'll see about answering them...

printing a message to stdout in fortran

2011-05-27T13:06:00.002+01:00

write (*,'(''I wonder how someone kept a straight face when they invented this syntax for writing a string to the console'')')

ruby cloudwatch -> mrtg interface

2011-05-21T10:48:00.001+01:00

I use mrtg to gather historical data on some of my servers. One of those servers lives in Amazon's Elastic Compute Cloud (EC2) and so is also monitored by Amazon CloudWatch.

Can I get cloudwatch data into mrtg?

mrtg has a fairly straightforward interface for plugging in arbitrary unix executables to collect data, so my first attempt was to use the main Java-based cloudwatch client to get data. that attempt started up one jvm for each metric collected, which massively overloaded my ec2 microinstance, keeping the load average around 3. pretty lame.

Amazon also provides a ruby interface. I had never programmed in ruby before, but its often interesting to learn a new language.

Here's what I ended up with.

First the config block for mrtg, which calls out to the ruby-mrtg-cloudwatch3 program that I wrote:

Target[cloudwatch_network]: `/home/mrtg/ruby-mrtg-cloudwatch/ruby-mrtg-cloudwatch3 NetworkIn NetworkOut AWS
/EC2 InstanceId=i-26bcaf51`
Title[cloudwatch_network]: Network traffic according to cloudwatch
options[cloudwatch_network]: growright,absolute,logscaleMaxBytes[cloudwatch_network]: 100000000

This gives a graph of network traffic according to cloudwatch. I can compare that alongside the network traffic graph for eth0 gathered from the local interface statistics. They should roughly match up, and they do (well hopefully they still do by the time you read this - these are live images):

According to the on-host network interface:

According to cloudwatch:

Now the actual ruby code:

#!/usr/bin/ruby1.8

require 'rubygems'
require 'AWS'

The two cloudwatch metric names, one that measures output data, one that measures input data, are give on the command line:

metrico=ARGV[0]
metrici=ARGV[1]

My code has hardcoded access keys at the moment which is a bit shitty:

ACCESS_KEY_ID='foo'
SECRET_ACCESS_KEY='bar'

Using the above credentials, a new cloudwatch object is made, @cw.

@cw = AWS::Cloudwatch::Base.new(:access_key_id => ACCESS_KEY_ID, :secret_access_key => SECRET_ACCESS_KEY, :server => "eu-west-1.monitoring.amazonaws.com" )

Each of the two metrics will be probed with the probe function. This uses a state file based on the metric name to get only readings which have not already been seen by this script. The two metrics use separate state files because cloudwatch doesn't give an atomic read for multiple metrics at once. The state file stores the time of the last seen reading. If there is no state file, we have to invent a time. There is a subtlety here: data does not appear in cloudwatch until around 5 minutes after its time stamp, so using the current time as an initial value results in not seeing any results. Instead, I go back about 15 minutes the first time, which will seems to be far enough back to get something.

def probe(metric)

  et = Time.now()

  statusfn="cloudwatch-"+ARGV[3]+"-"+metric+".status"
  if FileTest.exist?(statusfn) then

    f = File.new(statusfn, "r")
    tstring = f.gets
    ts = Time.parse(tstring)
    f.close
  else
    ts = et - 900 # needs to be more than 5 mins because otherwise we never get any data.
end

  res = @cw.get_metric_statistics(:measure_name => metric,  :statistics => 'Average,Sum', :namespace => ARGV[2], :period => 300, :start_time => ts, :end_time => et, :dimensions=> ARGV[3])

Now we're going to look at the rows that come back. Usually only one row will come back, if we're running this at about the same rate that cloudwatch is adding readings, but sometheres there will be more, or fewer.

In the case of network traffic, I want to return the sum of all readings for this metric. In other cases, such as disk usage, I would want to return the mean. This distinction is the same as default vs gauge measurements in MRTG.

samples = 0
  sum = 0
  avgsum = 0

  datapoints = res["GetMetricStatisticsResult"]["Datapoints"]

  lt = ts
  if datapoints.nil? then
   # nop
  else
    rows = datapoints["member"]

    rows.each { |r|
      nlt = Time.parse(r["Timestamp"])
      if(nlt < ts) then
        # nop - time was before requested start
      else
        samples += Float(r["Samples"])
        avgsum += Float(r["Average"])
        sum += Float(r["Sum"])
        nlt += 1
        if(nlt > lt) then
          lt = nlt
        end
      end
    }

Now we can write out the new state file:

f=File.new(statusfn, "w")
    f.puts(lt)
    f.close
  end
  return sum
end

and finally output the MRTG format information:

sumo=probe(metrico)
sumi=probe(metrici)

# output mrtg format
puts sumo
puts sumi
puts 0
puts "cloudwatch: "+metrico+" and "+metrici

The end.

UK electric sockets vs chopsticks

2011-05-14T05:13:00.000+01:00

My father taught me this trick when I was far too young to be taught this trick - how to connect a Europlug to a UK (actually HK in this case) electrical socket.

PAM python module for out-of-band one-time tokens

2011-05-07T18:00:00.002+01:00

I previous wrote about integrating openid with unix shell logins for my public shell server barwen.ch. This post talks about the out-of-band PAM token module that I wrote as part of that - where I'm generating the tokens when the user is authenticated by OpenID. But I guess it could also have use when there's some other out of band mechanism (such as sending something by SMS?)

Subject to some other non-PAM web-based authentication (openid in this case, but it could be anything really), I want to issue a token value to the user in-band with respect to that other authentication (i.e. in a web page shown to the user), which is out-of-band with respect to PAM. That token should then be usable for a short period of time to make a single PAM authorisation to sshd.

That is, if you can log into the web-based authentication, you should then be able to log into the ssh system.

So on one side I need a PAM module (which I will write in Python) to check the tokens, and on the other side I need something (a command line tool) to issue the tokens. To complete the loop, I need some database (the filesystem) to store the tokens on the server side.

So here's the code. The PAM module comes complete with documented security vulnerability which allows anyone to delete certain files on your file system. ho ho.

First the token creator:

#!/usr/bin/python

import base64
import os
import pickle
import sys
import time

VALIDTIME = 60

tokenbits = os.urandom(8)
token = base64.b64encode(tokenbits, "+-")

print token

fn = token + ".token"
fh = open(fn, 'w')

obj = (sys.argv[1], time.time() + VALIDTIME)

pickle.dump(obj, fh)

and secondly the PAM module, which is based on the PAM module in my previous post:

import os
import syslog
import pickle
import time

def pam_sm_authenticate(pamh, flags, argv):
  syslog.syslog("start benc")
  pamh.authtok
  if pamh.authtok == None:
    syslog.syslog("got no password in authtok - trying through conversation")
    passmsg = pamh.Message(pamh.PAM_PROMPT_ECHO_OFF, "Monkeyballs?")
    rsp = pamh.conversation(passmsg)
    syslog.syslog("response is "+rsp.resp)
    pamh.authtok = rsp.resp
  # so we should at this point have the password either through the
  # prompt or from previous module
  syslog.syslog("got password: "+pamh.authtok)

  # now look for token
  # SECURITY BUG TODO: we're using this to make a path so we need to make sure
  # we're not being directed out into some other directory. We know the
  # range of characters that can be used in a token so we can reject if
  # anything other than those exists.
  # Especially as we delete the token file on use - otherwise could delete
  # arbitrary files on the system...
  tfn = "/root/" + pamh.authtok + ".token"

  if os.path.exists(tfn):
    fh = open(tfn)
    tokendata = pickle.load(fh)
    tokenuser = tokendata[0]
    tokentime = tokendata[1]
    fh.close()
    os.remove(tfn);

    # will remove the token even if it was for the wrong user
    # not sure if there's any security different wrt leaving it there if
    # its the wrong user?

    if tokentime < time.time():
      syslog.syslog("token time expired")
      return pamh.PAM_AUTH_ERR

    if tokenuser != pamh.user:
      syslog.syslog("token user "+tokenuser+" does not match requested user "+pamh.user)
      return pamh.PAM_AUTH_ERR
    

    return pamh.PAM_SUCCESS

  return pamh.PAM_AUTH_ERR

def pam_sm_setcred(pamh, flags, argv):
  return pamh.PAM_SUCCESS

ssh-like login with openid

2011-04-26T15:53:00.006+01:00

I rigged together shellinabox and mod_auth_openid with some custom PAM glue so people can log into my hobby server s0.barwen.ch with an in-browser terminal window and openid.

shellinabox is not ssh (although web-based ssh is a good approximation). Instead it seems to be AJAX-over-https (which is kinda wtf for terminal access, but hey it seems to work).

The way I've glued it together is: First you visit the login page. That is an openid protected CGI script. The script runs with your openid in $REMOTE_USER, and does three things: it maps your openid to a local username; it generates (via sudo) an authentication token for you; and it HTTP-meta-redirects you to a hacked version of shellinabox.

shellinabox gives you a login prompt, asking for username and password. My hacked version stuffs the username and authentication token from the previous step into the keyboard.

The token ends up at a custom PAM module which verifies that the token is valid (for that user, and within a small time window after issue) and lets you in.

Then you get your shell prompt.

This seems like an interesting addition to barwen.ch's collection of login methods.

If you want a play, you can sign up at s0.barwen.ch

Also, if you break this, let me know rather than deleting / ...

pam_python

2011-04-23T16:36:00.001+01:00

I came across pam_python, a PAM module that lets you write PAM modules in Python. I've come across things scripted by python a couple of times in the last few weeks at work so it seems interesting to play in this direction.

The first module I got sort-of working is this, which lets anyone log in with the password poop53.

import syslog

def pam_sm_authenticate(pamh, flags, argv):
  syslog.syslog("start benc")
  at = pamh.authtok
  syslog.syslog("got password: "+at)
  if at == "poop53" : 
    return pamh.PAM_SUCCESS
  else:
    return pamh.PAM_AUTH_ERR

def pam_sm_setcred(pamh, flags, argv):
  return pamh.PAM_SUCCESS

Now this cheats a bit - it assumes that some other module has read in the password from the user - I used pam_unix to do that, configured as below, so that first a check against the unix password happens and then if that fails, check against poop53.

auth sufficient pam_unix.so
auth sufficient pam_python.so /root/auth.py

The specific use I am thinking of, I don't want unix passwords to work. So in that case, I need to read in the password myself if it isn't already set.

Here's how I made that work:

def pam_sm_authenticate(pamh, flags, argv):
  syslog.syslog("start benc")
  pamh.authtok
  if pamh.authtok == None:
    syslog.syslog("got no password in authtok - trying through conversation")
    passmsg = pamh.Message(pamh.PAM_PROMPT_ECHO_OFF, "Monkeyballs?")
    rsp = pamh.conversation(passmsg)
    syslog.syslog("response is "+rsp.resp)
    pamh.authtok = rsp.resp
  # so we should at this point have the password either through the
  # prompt or from previous module
  syslog.syslog("got password: "+pamh.authtok)
  if pamh.authtok == "poop53" : 
    return pamh.PAM_SUCCESS
  else:
    return pamh.PAM_AUTH_ERR

def pam_sm_setcred(pamh, flags, argv):
  return pamh.PAM_SUCCESS

To use this with sshd, I need to enable sshd options UsePAM and ChallengeResponseAuthentication, and now I get this:

$ ssh root@192.168.141.128
Monkeyballs?poop53
Linux alcf3 2.6.35-28-generic #49-Ubuntu SMP Tue Mar 1 14:40:58 UTC 2011 i686 GNU/Linux
#

So I'm happy that I can grab some string from the remote user now, and process it to get an authentication decision.

Thought its pretty weird to have a regular ssh client giving me a Monkeyballs? prompt at auth time...

Modified: 2011-05-08: Later I used pam_python to write an out of band token module

spam and fidonet

2011-04-16T15:14:00.000+01:00

I got a spam the other day, addressed to an address that isn't mine. That's not unusual. What was unusual was the address they used. It isn't mine, but it was mine when I was a teenager - benc@donor2.demon.co.uk was my internet address on DoNoR/2, an OS/2 focused BBS near Woking (in those days, young whippersnappers, you cared down to the town level where you were connecting to - DoNoR/2 was in dialing code 01483, the same as Guildford where I grew up). DoNoR/2 was primarily a fidonet system - 2:252/156, and then after the BS of geonetting, 2:440/4, and I was point 2 off that - Ben Clifford at 2:252/156.2

So although I'm usually annoyed when spam gets through my filters, this one made me think: aaah natsukashi.

Date: Thu, 27 Jan 2011 09:44:27 -0800 (PST)                                     
From: Jim Vivona                                            
To: benc@donor2.demon.co.uk                                                     
Subject: re                                                                     

sup! if you hadn't heard i lost my job at lawncare company about 5              
weeks ago, then i found this news article and made 379 in a few                 
hours!! I guess it was for the best! I learned from - News channel 4            
talk to you later!

or headers in full:

Return-Path:                                                
X-Spam-Checker-Version: SpamAssassin 3.3.1 (2010-03-16) on                      
dildano.hawaga.org.uk                                                       
X-Spam-Level:                                                                   
X-Spam-Status: No, score=-2.1 required=2.5 tests=BAYES_00,DKIM_SIGNED,          
DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,RCVD_IN_DNSWL_NONE,     
URIBL_BLACK autolearn=ham version=3.3.1                                     
X-Spam-ASN: AS36646 98.138.0.0/17                                               
X-Spam-tokens-ham: 0.000-57--100h-0s--0d--hadnt,                                
0.000-55--96h-0s--0d--hadn't,                                               
0.000-28--48h-0s--0d--lisa, 0.000-25--44h-0s--0d--Lisa,                     
0.001-19--32h-0s--0d--madison, 0.001-19--32h-0s--0d--Madison,               
0.001-18--31h-0s--0d--Wisconsin, 0.001-18--31h-0s--0d--wisconsin,           
0.001-9--15h-0s--0d--entrepreneurs, 0.002-124--220h-1s--0d--Fwd             
X-Spam-tokens-spam: 0.902-15425--22770h-653297s--0d--H*c:alternative,           
0.861-28--214h-4131s--0d--president,                                        
0.860-6821--59523h-1134787s--0d--H*Ad:D*uk                                  
X-Spam-relays-trusted:                             

X-Spam-relays-untrusted: [ ip=98.138.85.229                                     
rdns=web120502.mail.ne1.yahoo.com                                           
helo=web120502.mail.ne1.yahoo.com by=dildano.hawaga.org.uk ident=           
envfrom=                                                                    
intl=0 id=p0RHpCGr007860 auth= msa=0 ] [ ip=194.54.47.229 rdns= helo=       
by=web120502.mail.ne1.yahoo.com ident= envfrom= intl=0 id= auth= msa=0 ]    
X-Spam-dkim-identity: @yahoo.com vivonajj@yahoo.com                             
X-Spam-dkim-domain: yahoo.com                                                   
X-Spam-dccb: dcc1.aftenposten.no                                                
X-Spam-dccr: dildano.hawaga.org.uk 1215; Body=1 Fuz1=1 Fuz2=1                   
X-Spam-token-summary: Tokens: new, 1; hammy, 109; neutral, 84; spammy, 3.       
X-Spam-languages: en                                                            
X-Spam-autolearn: ham                                                           
Received: from web120502.mail.ne1.yahoo.com (web120502.mail.ne1.yahoo.com       
[98.138.85.229])                                                            
by dildano.hawaga.org.uk (8.13.8/8.13.8/Debian-3) with SMTP id              
p0RHpCGr007860                                                              
for ; Thu, 27 Jan 2011 17:51:14 GMT                     
Authentication-Results: dildano.hawaga.org.uk; dkim=pass (1024-bit key)         
header.i=@yahoo.com; dkim-adsp=none                                         
Received: (qmail 94875 invoked by uid 60001); 27 Jan 2011 17:44:27 -0000        
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.com; s=s1024;     
t=1296150267; bh=niep53FNFb78lkhNFkO8MX4NIpOCMZRTAUTHm1+GJzQ=;              
h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Ver    
sion:Content-Type;                                                          
b=OWa2WgmhLxGRa+pJep7Or929UysoVIk/SCB7BnFfurvysB63Nr6Odfb4b3gm2hFZqK+xOo    
Q6aZmUXn27EQbeA/8av52fU1KV33uhA9Th6rI0uKEIPg5LikGLLXUoaXrLzGdL2qyJ10UTMy    
2TwEkqU6bZQBCpMxY0fWANKPiIK+M=                                              
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws;                                
s=s1024; d=yahoo.com;                                                         
h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Versi    
on:Content-Type;                                                            
b=eIuzjdEYirBi9RTFb1voGAKkH4bQUYyRkN6NT6mDBMj2GJcnf8bKz7R7NrQuWd8j9tjoviMF    
bXv/t3D2DtcoNbvQuDSPMa6ycXDMUkNFpW3dMkyrq6ZBSuw+Ye7TZXH7ect5MJcErjTAyu38    
+Dx4kXmdFIlAhs3Q0CBs4L7t+EI=;                                               
Message-ID: <164580.94308.qm@web120502.mail.ne1.yahoo.com>                      
X-YMail-OSG: vT0rPzMVM1kHrbVNywVWrHu0pysHCRnEnLjmjnEWPDU8KWm                    
9AZTRLoDJBmvlFuAhJxD2.uKxh0LPBsJi.WmUQZBW_OOq9UKFRzUPfKAOemv                 
qni6KAcfSaxd8Y6p2Cf6w5PGXAILIpD_0UuPIQ3LtnYoffxsz6w1ytx9R3cG                   
BiqUC4MNLdG0NlSV2mlQCFGOEBHXYNTzl4ejOnjciku0Z1Y5SGW4aUz_4gmA                   
oWXR.IhJ4dfWwgEVx2H9GvVpuPLizb_vwjmqP1e02TP9qrN0cGC1tFWTbyW9                   
ooJoemIjAwkiYhhY-                                                              
Received: from [194.54.47.229] by web120502.mail.ne1.yahoo.com via HTTP; Thu    
, 27 Jan 2011 09:44:27 PST                                                  
X-Mailer: YahooMailRC/553 YahooMailWebService/0.8.107.285259                    
Date: Thu, 27 Jan 2011 09:44:27 -0800 (PST)                                     
From: Jim Vivona                                            
Subject: re                                                                     
To: benc@donor2.demon.co.uk                                                     
MIME-Version: 1.0                                                               
Content-Type: multipart/alternative;                                            
boundary="0-588940240-1296150267=:94308"                                    
X-Greylist: Delayed for 00:06:40 by milter-greylist-3.0                         
(dildano.hawaga.org.uk [81.187.211.37]); Thu,                               
27 Jan 2011 17:51:15 +0000 (GMT)

roman numerals code

2011-04-09T21:21:00.002+01:00

I made this roman numeral convert applet years ago (the RCS tag is $Id: Roman.java,v 1.11 2001/01/07 15:12:00 benc Exp $ ) and mostly left it untended since then. It accounts for 25% .. 50% of the hits on hawaga.org.uk and was brought to the front of my consciousness by someone asking if they could use the source in their school project. Now I feel all embarrassed about the clunky UI on that thing.

holon

2011-04-02T11:30:00.000+01:00

Word of the day is holon - a thing that is both a whole in itself, and a component of something bigger. This is what a part of a hierarchical system is - both something clearly distinguishable from the rest of the system (in which case it is a distinct whole), but still part of that system.

sshfp dns

2011-03-26T12:36:00.001Z

I've set up DNSSEC, so I'm on the path to trusting DNS more. I can put SSH key fingerprints for my hosts into DNS, and SSH clients can check those.

Even with insecure DNS, this is probably better than what you do now, which is to just to choose 'yes' to the following prompt without actually checking: (seriously, do you ever bother?)

The authenticity of host 's0.barwen.ch (192.168.55.55)' can't be established.
RSA key fingerprint is 9e:81:ab:cb:2a:ad:26:2f:10:ed:dd:5c:55:dd:ea:58.
No matching host key fingerprint found in DNS.
Are you sure you want to continue connecting (yes/no)?

SSH can check s0's DNS record to see if a fingerprint is stored there, and tell you if it matches. So lets set that up.

I need to add an SSHFP record to the DNS for s0.barwen.ch.

On host fubar (without needing to be root):

$ ssh-keygen -r s0.barwen.ch
s0.barwen.ch IN SSHFP 1 1 560f08c1687a60e62a65ef427e63698ae1797d6f
s0.barwen.ch IN SSHFP 2 1 4ef38fd457d0afec50ca21eacb771f724e6d7236

So those are the records to add to barwen.ch's DNS.
(btw, vim on my machine doesn't like SSHFP records and highlights everythign red - eww)

Now wait for DNS to settle, and when I connect for the first time, I get a different message (my emphasis).

The authenticity of host 's0.barwen.ch (192.168.55.55)' can't be established.
RSA key fingerprint is 9e:81:ab:cb:2a:ad:26:2f:10:ed:dd:5c:55:dd:ea:58.
Matching host key fingerprint found in DNS.
Are you sure you want to continue connecting (yes/no)?

Cool.

You might need to set the client option VerifyHostKeyDNS ask in your ~/.ssh/config - if you really trust DNS, you can set it to yes instead, and it won't even ask you when there's an SSHFP record present.

You can try this yourself, even without a user account, because host key verification happens before user authentication: ssh -o 'VerifyHostKeyDNS ask' s0.barwen.ch

ASCII

2011-03-19T13:00:00.002Z

An ASCII character walks into a bar.
The bartender says "What's the problem?"
The ASCII character says, "I have a parity error."
The bartender nods, and says, "Yeah, I thought you looked a bit off."

time for visa transaction dispute!

2011-03-17T12:16:00.001Z

so I took my laptop back to a-mac utrecht, as its still got its crash-every-three-days problem. They refused to either refund the money or replace the laptop with a new one. Whilst they said they would talk to apple about a replacement, this has gone far enough for a product that was defective as sold, so I'm going to take advantage of the transaction protections I apparently get from the consumer credit act (and Visa), and dispute the transaction.

I got a lovely comment from the manager of the store when I said that I would expect a kernel crash every one to two years not every three days, that he would expect it to never happen. Which is funny in a "yes we sold you crap but we won't fix it" way.

numbering commits

2011-03-11T22:10:00.001Z

svn gives each commit a unique number. mercurial does somethign similar. CVS doesn't. git has commit IDs btu they are big and dont' have an intrinsic order (if you dehash two commit IDs you can figure out relative order but its not apparent from the IDs themselves)

I'm interested in numbering the commits on a git branch that is imported from CVS, so there's a well defined linear order (unlike in git in general).

I hacked together this script:

#!/bin/bash

COMMITCOUNT=$( git rev-list origin | wc -l)

echo There are $COMMITCOUNT commits on the origin branch

# this strips whitespace
export COUNT=$(($COMMITCOUNT))

git rev-list origin | while read commitid ; do
  echo numbering $commitid as $COUNT
  TAG=cvs$COUNT
  git tag $TAG $commitid
  COUNT=$(( $COUNT -1))
done

which works like this:

$ ./number-cvs 
There are 205 commits on the origin branch
numbering fea9db3bc7b3e36f82a97d3bb194eb60ecb3b57f as 205
numbering aedbfe81cc1dbf3d6f833225aa41826854398a3c as 204
numbering f040d23565211acb637d3325d240d675fe1e61a6 as 203
numbering eef4a46ce30de2836402a373e8eae49fc1b75935 as 202
numbering 2bb5b931be9beb0d90a2796b85585149465f8fc3 as 201
numbering a4372569c60bcb6d92a63b258389b5f1a210dd40 as 200
fatal: tag 'cvs200' already exists
numbering bbd6af71ef17fcb05a9cf86a372837dcf470e30b as 199
fatal: tag 'cvs199' already exists
numbering 6e1dc4d7d59b3515a3f46c17517c1bb85172c7bc as 198
fatal: tag 'cvs198' already exists
numbering 87c59d4b1bf4c7b1bcb64af078a66290d74f6ebf as 197
fatal: tag 'cvs197' already exists
[...]

This being a hack, I don't attempt to handle previously tagged revisions and instead let git tag give a fatal error that isn't really fatal...

Now I end up with commit tags that look like cvs200, cvs201, ...

last repair attempt which pretty much says they did nothing actually seems to have done nothing

2011-03-11T11:20:00.000Z

Well, it took about 46h from my Mac being returned to me for it to crash again. I won't be in Utrecht until next Thursday so I can't take it back to a-mac to grumble some more until then.

result of 2nd repair

2011-03-08T08:24:00.003Z

after the previous failed attempt to make my new mac work, the 2nd repair attempt of my new mac is reported as:

Uitvoerig getest . weer waren er kleine problemen op de schijf
ditmaal konden ze wel hersteld worden
Ik zie aan de log files dat de kernel panic puur om software gaan en
niet hardware.
deze problemen zijn hersteld , en de Macbook werkt weer prima
voor een goede test zal ik de mac nog door testen 
 Na diverse testen werkt de Macbook prima geen verdere problemen

07-03-2011 Aan de log files van de machine te zien heeft het probleem
te maken met het feit dat er een Backup is terug gezet , waarvan de
fouten waarschijnlijk mee over zijn gekopieerd
Na herstel van de Harddisk * software ( werkt hij prima

which in a one-liner is "we found some corrupted files and repaired them. this is a software problem. it works fine now."

To be honest, that sounds like complete BS given the symptoms and the actions taken for previous repair (meaning its had at least two separate OS installs on two different hard-drives)... plus yes "it works fine" most of the time - just it crashes every 3 or 4 days. As the mac has been in their possession for repair for only 3 days, and I'm sure they haven't been using it as much as I do during that time, I don't think they can accurately state that it works now. The next week should tell, though.

In the meantime, Apple sent me a questionnaire about the previous repair attempt which gave me the opportunity for further grumbling (can you tell I'm English?).

-- later --

got laptop back - total result of repair: some screen dumps of them running the disk repair utility, and they wiped some fingerprints off the screen. lets see if that fixed the problem. <cough;>

ssh over CONNECT over port 80

2011-03-05T13:16:00.000Z

I run an ssh server on port 443 (the https port) of one of my machines. That's good when I want to get ssh from a network which bans "everything but web-browsing" - once I have ssh I can tunnel pretty much what I want.

But the other day I ran across a network (at an airport) which allowed only port 80 - the regular http port. Even port 443 was banned (so not only could I not connect to my ssh server, but no facebook, gmail, etc...)

I already have stuff on port 80 - my webserver - so what could I do? I know ssh can be tunnelled through the http CONNECT method. Could I set that up so that my web server would serve web traffic as usual but allow me to CONNECT to the ssh server?

Turns out yes.

In the http server config - enable mod_proxy and mod_proxy_connect. Then this config in proxy.conf (or the main server config, I guess):

<IfModule mod_proxy.c>
         ProxyRequests On
        <Proxy *>
                AddDefaultCharset off
                Order deny,allow
                Deny from all
        </Proxy>
        <Proxy localhost>
          Allow from all
        </Proxy>
        AllowCONNECT 22
        ProxyVia On
</IfModule>

(If you're doing this yourself - be careful about what you allow - if you are too liberal you turn your server into an open spamming and hacking engine for the world to exploit. And it will be found. Automatically, and within days or maybe hours.)

On the client side, use netcat as a proxy command in SSH: (you can also put the proxy command in ~/.ssh/ssh_config)

ssh -o 'ProxyCommand nc -X connect -x myhost.example.com:80 localhost 22' myhost.example.com

Tada.

Note that the ssh server now sees you connecting from localhost, and the http server is the one who logs the real IP address. A caveat here is if you have IP-based security policies that make localhost special, then anyone connecting through this proxy is also special.

Lots of the config for this came from http://mariobrandt.de/archives/technik/ssh-tunnel-bypassing-transparent-proxy-using-apache-170/

So that gets me a CONNECT proxy.

But does it work at the airport? No.

Turns out the airport is also running everything through a transparent proxy: when I connect to s0.barwen.ch port 80, I'm actually connected to the airport's transparent proxy. So an http CONNECT command to localhost:22 both points to the wrong place and is administratively prohibits.

It turns out I can http CONNECT to s0.barwen.ch port 80, though, and there issue another CONNECT command to get to localhost:22:

$ nc -4 -X connect -x s0.barwen.ch:80 s0.barwen.ch 80 
CONNECT localhost:22
HTTP/1.0 200 Connection Established
Proxy-agent: Apache/2.2.14 (Ubuntu)

SSH-2.0-OpenSSH_5.3p1 Debian-3ubuntu5

So I can get to the server this way.

How can I get the ssh commandline to talk to the remote server, with the extra proxy step added?

Like this:

$ cat t.sh 
( echo "CONNECT localhost:22" ; cat ) | nc -X connect -x s0.barwen.ch:80 s0.barwen.ch 80 | ( read ; read ; read; cat)

$ ssh -o 'ProxyCommand ./t.sh' s0.barwen.ch

Now once that's done, I can run a SOCKS proxy over the same ssh connection, and route my normal web browsing through that - giving me access to https sites, and anything else that can use SOCKS.

disappointing new mac

2011-03-04T10:28:00.004Z

Well my last mac died, as they do every now and then. So I activated my usual replacement behaviour: go to nearest mac store (in this case, Amac in Utrecht) and buy a new macbook.

Alas this new macbook started BSODing every few days, usually after a resume. So I took it back to the shop. They took it off for repair and diagnosed it with a faulty hard drive (?) and returned it after a week with a new HD.

Macbook still BSODs ever few days.

So back to the shop again. I thought maybe this time they'd give me a real replacement. No they want to take it off for repair again. I wonder if some dude has to sit in a room repeatedly suspending it and unsuspending it for a week to try to reproduce? Presumably it'll come back in a week with "cannot reproduce" and then it will continue crashing for me and then I will have to go argue with them lots?

This is a disappointingly slow and lame process which is not what I expected from either a Mac or from a Premium Reseller. grumble.

dnssec: automated re-signing of hawaga.org.uk

2011-02-27T14:16:00.002Z

In a previous post on DNSSEC-signing my zone hawaga.org.uk, I mentioned that signatures will expire after 30 days, and so I (or rather one of my computers) will need to re-sign the zone at least every month.

Basically I need to run the dnssec-signzone command again, but there is some dancing around that needs to happen.

The most awkward was that I need to increment the zone serial number in the SOA record of my zone. Previously I've maintained this by hand, keeping it in format YYYYMMDDNN (year, month, day, sequence-number-on-that-day). That format is quite appealing because even if I forget what number I got up to, I can wait a day and know that I have a number in sequence.

dnssec-signzone offers a couple of options for doing things to serial numbers, but neither was what I wanted: one will increment the input SOA by one, but I want to maintain a pristine source zone file; another will set the SOA to the number of seconds since the unix epoch. This changes the format away from what I want.

So I wrote a quick utility, soatick, to generate zone serial numbers based on the current time and a state file, so that each invocation will generate a new serial number matching the format that I want:

$ ./soatick
2011010901
$ ./soatick
2011010902
$ ./soatick
2011010903

Now I'll use the m4 macro processor to put this in place before signing the zone:

export NEWSERIAL=$(/home/benc/src/soatick/soatick )
m4 -D___SERIAL___=$NEWSERIAL < db.hawaga.template > db.hawaga.generated
/usr/sbin/dnssec-signzone -S -t -a -l dlv.isc.org -f db.hawaga.signed -o hawaga.org.uk db.hawaga.generated

I put the above in a script called from cron, and set it to run every week.

Now a weakness here is that I have to keep my signing key unpassworded and on a system connected to the internet. The zone-signing and key-signing key separation should help here, by allowing me to keep a more important key offline and a less important key online, but I haven't investigated it in any greater depth - perhaps I should...

public nmap server

2011-02-19T07:35:00.000Z

Well, I put up a public nmap server on barwen.ch that will nmap whatever address you are connecting from in your browser. I really wonder what the bad uses and the good uses (if any) this can be put to are. It was at least funny to watch yahoo and google hammer on it 'till I put a robots.txt in place.

choosing a password

2011-02-13T09:34:00.002Z

many sites want a password. for a lot of middle-to-low security accounts, I keep a(n encrypted) database of passwords on my computer, rather than making them memorable or using the same one on all. So I cut and paste each password and don't care about it being easily typable. To generate the passwords, I use a command-line like this:

$ cat /dev/random | strings -n 16
:*jx4%8er:>kRKh:
a#ka;lPB6rB9SX";lk
6B!'X@Q{@QQ LZB?
hZ if=A2u3;-S]v?P
Ix6RwEwqVqEg~0fFi
[hkE*0T~GZX^5=h<4

Using mrtg and iptables to record IPv4 vs IPv6 traffic

2011-02-06T09:59:00.001Z

I wanted to plot IPv6 vs IPv4 traffic on my hosts - I have most services enabled for IPv6 but I know they don't get used much. I had MRTG already.

iptables on Linux counts bytes that pass through it, even if there are no iptables rules:

$ iptables -L -v -x
Chain INPUT (policy ACCEPT 6079694 packets, 2474020715 bytes)
[...]

That counts ipv4 packets. The ipv6 equivalent is ip6tables.

So without needing to add any iptables rules at all, I can feed this output to mrtg with a script as follows, which outputs IPv4 traffic (for all three categories) as the first (input) variable, and IPv6 as the second(output) variable.

#!/bin/bash
A=0
IP4=$(/sbin/iptables -L -x -v | grep -e ^Chain | sed 's/.* \([0-9]*\) bytes)$/\1/' | ( while read n ; do A=$(( $A + $n )) ; done ; echo $A))

A=0
IP6=$(/sbin/ip6tables -L -x -v | grep -e ^Chain | sed 's/.* \([0-9]*\) bytes)$/\1/' | ( while read n ; do A=$(( $A + $n )) ; done ; echo $A))

echo $IP4
echo $IP6
echo 0
echo unknown

On one host, there really is hardly any ipv6 traffic (2 bytes/sec!) so I turned on the log scale plot option in MRTG to show the ipv6 a bit more (though to be honest its still pretty invisible).

Here's the config I used in MRTG to call the above script:

Target[ip46]: `/home/benc/bin/iptables-to-mrtg`
Target[ip46]: `curl http://dildano.hawaga.org.uk/mrtg-iptables.txt`
options[ip46]: growright,logscale
MaxBytes[ip46]: 1000000000000
Title[ip46]: IPv4 vs IPv6
YLegend[ip46]: bytes/sec
LegendI[ip46]: IPv4
LegendO[ip46]: IPv6

and here's an example graph (live, click for historical data):

Caveats:

I'm summing the all three iptables chains: input, output, and forwarded, for all interfaces. So some traffic here can be counted unexpectedly: A forwarded packet traverses all three chains (I think) so this is not a good way to count traffic if your linux box is a router; The lo interface will also be counted, so traffic to localhost (127.0.0.1 or ::1) will be counted in this graph. This might be useful to remove.

When there's a tunnel endpoint on the machine, then traffic to that tunnel will be counted twice: one as it passes the tunnel interface, and once as the encapsulated form passes the physical ethernet interface.

These are not insurmountable, I think: by setting specific iptables rules that address these concerns and counting traffic from those instead of the main chain counters.

dnssec: signing hawaga.org.uk

2011-01-29T09:41:00.000Z

In this post I will sign my main DNS zone hawaga.org.uk using DNSSEC so that other resolvers can verify the contents when they make a DNS lookup.

The parent domain org.uk does not do DNSSEC at the moment so I am going to use DLV (DNSSEC Lookaside Validation). DLV will let me publish my zone public keys in DLVs registry instead of in the parent org.uk zone, and my zones will be validated by anyone who has configured DLV in their resolver, rather than by all DNSSEC users (pretty much the first is a strict subset of the second). This is something of a hack - hopefully in a few months org.uk will support DNSSEC and I'll be able to directly publish my keys there instead.

Most of what follows works for both normal DNSSEC and DNSSEC-with-DLV.

I need to generate two public/private keypairs: a zone signing key, and a key signing key. The key signing key will be used to sign the zone signing key, and the zone signing key will be used to sign the records inside the zone. Its not entirely clear to me which private keys need to be online at which step in the process, but for my immediate purposes I don't mind too much - I'm keeping everything online the whole time for now.

bind comes with a utility called dnssec-keygen to generate the keys, and it is used much like any other command-line key generator such as gpg oropenssl:

$ /usr/sbin/dnssec-keygen -a RSASHA1 -b 768 -n ZONE hawaga.org.uk
Generating key pair...................++++++++ ..++++++++
Khawaga.org.uk.+005+48075
$ /usr/sbin/dnssec-keygen  -f KSK -a RSASHA1 -b 2048 -n ZONE hawaga.org.uk
...
$ ls Khawaga*
Khawaga.org.uk.+005+48075.key      Khawaga.org.uk.+005+48196.key
Khawaga.org.uk.+005+48075.private  Khawaga.org.uk.+005+48196.private

Now, I'm going to sign the zone:

$ /usr/sbin/dnssec-signzone -S -l dlv.isc.org -o hawaga.org.uk db.hawaga 
Fetching KSK 48196/RSASHA1 from key repository.
Verifying the zone using the following algorithms: RSASHA1.
Zone signing complete:
Algorithm: RSASHA1: KSKs: 1 active, 0 stand-by, 0 revoked
                    ZSKs: 1 active, 0 stand-by, 0 revoked
db.hawaga.signed

and I get these output files:

-rw-r--r-- 1 benc benc 35505 2011-01-04 21:47 db.hawaga.signed
-rw-r--r-- 1 benc benc   195 2011-01-04 21:47 dlvset-hawaga.org.uk.
-rw-r--r-- 1 benc benc   171 2011-01-04 21:47 dsset-hawaga.org.uk.

The signed zone lives in db.hawaga.signed. It looks like my input zone but with some new records added. For every input records, there is a new RRSIG record; there are DNSKEY records which contain the public keys generated above; and there are NSEC records which are used to securely deny the existence of entries.

In my bind directory, I replace my original db.hawaga zone file with the new signed version and restart bind.

Now bind will serving the appropriate DNSSEC records. I can see them by querying using the +dnssec flag to dig:

$ dig +dnssec www.hawaga.org.uk
[...]
;; ANSWER SECTION:
www.hawaga.org.uk.      3600    IN      CNAME   paella.hawaga.org.uk.
www.hawaga.org.uk.      3600    IN      RRSIG   CNAME 5 4 3600 20110208095742 20110109095742 48075 hawaga.org.uk. lNdWf71In/J8F7evBxxi1yTw7Fx4WRkcHK9vOilEyLmDq31uwYlTtf+d bAZ4WHSeF9aHGRlvy1c6bAWEgWs64K8RNr/7pkZW+y0kmP8qL+Eu0nOH DvvQQ32eShnoEYGc
paella.hawaga.org.uk.   3600    IN      A       174.143.245.7
paella.hawaga.org.uk.   3600    IN      RRSIG   A 5 4 3600 20110208095742 20110109095742 48075 hawaga.org.uk. EeUBihcnpDJad9JJnwLcR0nm9ef1E58fxdwio/SK1iSorkFZLZjxvk7r GYkCR0aCwAw1F2/lJ3kb6pTk+10H00lyowQc8crtBPIDkwiqDE0pTtEE JPCm51XuAc3bz/lX
[...]

So now my zone is signed.

But! (and this is a big but) there is no trust path for any resolver to validate that - there is no reason for any resolver to believe that it really was *me* that generated the keys rather than some random attacker.

In X.509, certificate authorities tell you how to trust someone by signing certificates. In plain DNSSEC, the parent zone acts as a CA by providing a signed DS (delegation signer) record in addition to an NS record. In DLV, ISC's DLV service fills this role by providing the signed DS record.

I'm going to use ISC's DLV zone (which appears to be the only serious one). There's a web interface to sign up, at https://dlv.isc.org/. When you sign up there, the interface authenticates your ownership of the zone by giving you a cookie TXT record to put in your zone. Once that authentication has happened, you can upload a DNSKEY, DS or DLV record.

Then ISC will publish a DLV record set for you (presumably it constructs one for you if you give a DNSKEY or DS record?). For example, mine looks like this:

hawaga.org.uk.dlv.isc.org. 877  IN      DLV     48196 5 2 FD144A3B36AC7E939DD7A04D5C6F967A07D01FB0029CA8B440F6CC2D 6F2415B8
hawaga.org.uk.dlv.isc.org. 877  IN      DLV     48196 5 1 0DE399B36303676F1243A923B6FC3893AE248F90

It takes a few hours for that DLV record to appear, but when it does, that is enough for a DLV-enabled resolver to be able to authenticate.

DNS-OARC has some open DNSSEC-enabled resolvers that can be used for testing this. I can check my DNSSEC using one of them:

$ dig +dnssec @2001:4f8:3:2bc:1::64:20 -t a www.hawaga.org.uk
[...]
;; flags: qr rd ra ad; QUERY: 1, ANSWER: 4, AUTHORITY: 3, ADDITIONAL: 5
[...]

and look out for the ad bit to appear in the flags field. It does, which means that resolver trusts my results.

OK. That's the setup pretty much done. Two last notes:

Firstly, when a bind resolver is authoritative for a zone, then it won't check signatures and give an ad flag on results for that zone. That left me puzzling for a while, wondering why it wasn't checking my results, and is why I have to use one of DNS-OARC's resolvers above.

Secondly, this zone is only signed for 30 days. After that period (specifically, 30 days after I ran the dnssec-signzone command), the signatures will become invalid. This is quite a change from my previous non-DNSSEC zone update habits - I changed my zone a few times per year and only when I needed a change, but now I'm going to need to update it at least every month, and inaction will cause it to break. In a subsequent post, I'm going to write about some of the automation I did to do this.

dnssec: Configuring my resolver

2011-01-22T18:16:00.000Z

DNSSEC, a mechanism for securing DNS, has around for a long time but only in the last year or so has it seen serious deployment. The root zone was signed about 6 months ago, which provides a security root from which all other DNSSEC can flow. Last time I looked at DNSSEC that was far in the untimetabled future, so I didn't put much effort then to get it actually working.

In this post, I'm going to write about configuring bind to check DNSSEC when I make DNS queries. In later posts, I'll write about the other side of things: securing my own zones with DNS.

I mentioned the root zone being signed above. That's one way of checking DNSSEC signatures (and in the long term, the main way). Another way is DLV (DNSSEC Lookaside Validation) which acts as a certificate authority, providing a way for a DNS zone to be signed without having to have a path all the way from the root. A third way is by listing the keys for known domains, which allows everything under those domains to be validated without needing a signature from a higher level in DNS. (This third way is how IANA's Interim Trust Anchor Repository worked, before being superseded by the signing of the root zone).

I want to configure both validation from the root, and DLV.

I very roughly followed along with this page, though different versions of bind, and differences in what I want to do, lead to differences.

First I need the root key-signing (public) key. This is the single well-known value that must be securely obtained. So I use insecure DNS to obtain it:

$ dig . dnskey | grep "257 " > root.dnskey
$ cat root.dnskey
.                       172363  IN      DNSKEY  257 3 8
AwEAAagAIKlVZrpC6Ia7gEzahOR+9W29euxhJhVVLOyQbSEW0O8gcCjF
FVQUTf6v58fLjwBd0YI0EzrAcQqBGCzh/RStIoO8g0NfnfL2MTJRkxoX
bfDaUeVPQuYEhg37NZWAJQ9VnMVDxP/VHL496M/QZxkjf5/Efucp2gaD
X6RS6CXpoY68LsvPVjR0ZSwzz1apAzvN9dlzEheX7ICJBBtuA6G3LQpz
W5hOA2hzCTMjJPJ8LbqF6dsV6DoBQzgul0sGIcGOYl7OyQdXfZ57relS
Qageu+ipAdTTJ25AsRTAoub8ONGcLmqrAmRLKBP1dfwhYB4N7knNnulq
QxA+Uk1ihz0=

Now at this point I should carefully check that this is right against various out-of-band sources. I didn't bother.

I also want a trusted key for DLV. That is available here.

Next I need to tell bind about these keys. I'm going to use bind's managed-key mechanism for this.
I put the key material into a file called benc-managed-keys, like this:

managed-keys {
   dlv.isc.org. initial-key 257 3 5 "BEAAAAPHMu/5onzrEE7z1egmhg/WPO0+juoZrW3euWEn4MxDCE1+lLy2 brhQv5rN32RKtMzX6Mj70jdzeND4XknW58dnJNPCxn8+jAGl2FZLK8t+ 1uq4W+nnA3qO2+DL+k6BD4mewMLbIYFwe0PG73Te9fZ2kJb56dhgMde5 ymX4BI/oQ+cAK50/xvJv00Frf8kw6ucMTwFlgPe+jnGxPPEmHAte/URk Y62ZfkLoBAADLHQ9IrS2tryAe7mbBZVcOwIeU/Rw/mRx/vwwMCTgNboM QKtUdvNXDrYJDSHZws3xiRXF1Rf+al9UmZfSav/4NWLKjHzpT59k/VSt TDN0YUuWrBNh";
   . initial-key 257 3 8 "AwEAAagAIKlVZrpC6Ia7gEzahOR+9W29euxhJhVVLOyQbSEW0O8gcCjF FVQUTf6v58fLjwBd0YI0EzrAcQqBGCzh/RStIoO8g0NfnfL2MTJRkxoX bfDaUeVPQuYEhg37NZWAJQ9VnMVDxP/VHL496M/QZxkjf5/Efucp2gaD X6RS6CXpoY68LsvPVjR0ZSwzz1apAzvN9dlzEheX7ICJBBtuA6G3LQpz W5hOA2hzCTMjJPJ8LbqF6dsV6DoBQzgul0sGIcGOYl7OyQdXfZ57relS Qageu+ipAdTTJ25AsRTAoub8ONGcLmqrAmRLKBP1dfwhYB4N7knNnulq QxA+Uk1ihz0=";

};

Note that the format is different from the key files obtained - the IN DNSKEY keywords go away and initial-key goes in instead, and the key material is now quoted with " and with a ; at the end of the line.

Then I told bind to import this into its configuration:

$ grep benc-managed-keys *
named.conf:include "/etc/bind/benc-managed-keys";

I need to tell bind to start using dnssec by adding these to named.conf.options:

dnssec-enable yes;
dnssec-validation yes;
dnssec-lookaside auto;

Now restart bind and hope that it all works.

How can I test my setup? I can use dig with the +dnssec parameter. This adds a flag to the query saying that DNSSEC is desired. For example:

$ dig @192.168.1.254 +dnssec hawaga.org.uk

dig will give a flag line in its output, like this:

;; flags: qr rd ra; QUERY: 1, ANSWER: 0, AUTHORITY: 4, ADDITIONAL: 1

If DNSSEC was able to check the results (which means that the result was signed, and that the resolver that you just queried was able to validate the results, then there will be another flag in there: ad. If not, then something didn't work correctly.

You can get more DNSSEC logging by adding this to named.conf:

logging {
           channel dnssec_log {             // a DNSSEC log channel
                     file "/var/log/bind/dnssec.log" size 200m;
                   print-time yes;        // timestamp the entries
                     print-category yes;    // add category name to entries
                   print-severity yes;    // add severity level to entries
                     severity debug 3;      // print debug message <= 3
   
             };
   
       category dnssec  { dnssec_log;  };
     };

So that's DNSSEC configured for resolving. Next, I want to sign my own zones so that others can verify them with DNSSEC on their own resolvers - I'll write about that in another post.

IPv6 in Amazon EC2

2011-01-14T13:26:00.013Z

Amazon declares that IPv6 is unsupported on EC2 (the Elastic Compute Cloud), but I wanted it anyway. Here's two ways I got it: using 6to4 and using a tunnel from Hurricane Electric. In short, the winner was Hurricane.

I did everything below on one of the example Linux instances supplied by Amazon, with an elastic IP address attached.

The first approach I tried was using 6to4 - a protocol which automatically gives anyone with a static IPv4 address their own range of IPv6 addresses. In another blog post, I described how to get 6to4 running on Linux in 5 command lines. I ran those commands on my EC2 instance and end up with my own IPv6 address.

There were, however, some reachability problems. Its not clear to me how much of that comes from EC2 (for example, I tried to disable their firewall as much as possible, but its not clear how disabled it is), and how much it comes from the flakiness of 6to4. (see, for example, that Google doesn't support ipv6 over tunnels).

I have two IPv6 hosts already, one on 6to4 (P), one with native connectivity (D).

I can ping from my EC2 host to my own host P. Pinging from P to EC2 gives no response *until* I start a ping from EC2 to P, in which case I start getting responses. That makes me think very much that Amazon is running a stateful firewall for protocol 41 that allows traffic back in once something has been sent out, for any particular IPv4 address.

I cannot ping at all between D and EC2, in either direction.

From this online ping tool I can ping my EC2 instance OK.

The second method I tried is a manually configured tunnel via Hurricane Electric. HE have been around a long time and have a good reputation (and who I used before years ago). The configuration is a set of fairly straightforward web forms. I allocated a /64 (even that is excessive - I only need a single IPv6 address for this host)

The web form also gives example configuration instructions for a variety of platforms - The Linux-net-tools instructions are the ones I want. I pasted the 4 given commands literally into a root prompt on my EC2 machine, and that was all I needed for my machine to be connected (at least until reboot).

I see similar "stateful firewall" behaviour as I mentioned above, but they difference is that that is only be between me and the HE tunnel endpoint - as long as *anything* goes over the tunnel, then connectivity with the entire IPv6 world stays up. And when that tunnel is up, the connectivity from machines D and P seem *much* better. As in: I can ping both ways without any mysterious losses. So it looks like I'll need a ping to the tunnel endpoint (or anywhere, really) every minute or so. That's no big deal - I have MRTG set up to measure some ipv6 latencies anyway, and that suffices.

So HE is a little bit (a few web forms) more effort to set up. But the connectivity is much much better. I recommend HE over 6to4 for this.

Other links: aco wrote about getting IPv6 on EC2 using sixxs, and if you're interested in getting a shell account on this machine to try for yourself: www.barwen.ch

Modified: 2011-04-19 Rephrasing a bit based on ongoing experience, and some more hyperlinks

6 to 4 in 5

2011-01-14T13:25:00.000Z

I have native IPv6 on my LAN for one server. I have another server which lives on LAN with only native IPv4. Can I get IPv6 on that? Yes!

My present configuration uses 6to4. This is a very straightforward mechanism to configure on linux, without needing any setup outside of my own machine. On the downside, it gives very little control of routing which can lead to strange connectivity problems that are hard to debug.

I followed the
Linux IPv6 HOWTO howto pretty faithfully.

I needed these 5 steps:

$ ipv4="174.143.245.7"; printf "2002:%02x%02x:%02x%02x::1" `echo $ipv4 | tr "." " "`

This tells me that my prefix is: 2002:ae8f:f507::/48

I get a 16-bit (4 hex-digit) subnet number to pick my own networks (I'll pick 2 in this case, fairly arbitrarily), and then the remaining 64 bits go towards identifying the host on the network (which I'll pick 0123:4567:89ab:cdef. Another good choice would be ::1)

So I end up choosing the IP address: 2002:ae8f:f507:2:0123:4567:89ab:cdef

Next:

modprobe sit  (it was compiled but not loaded)
ifconfig sit0 add 2002:ae8f:f507:2:0123:4567:89ab:cdef/16 up
/sbin/route -A inet6 add 2000::/3 gw ::192.88.99.1 dev sit0

and now I can ping my own machine:

benc@paella:~$ ping6 dildano.hawaga.org.uk
PING dildano.hawaga.org.uk(dildano.hawaga.org.uk) 56 data bytes
64 bytes from dildano.hawaga.org.uk: icmp_seq=1 ttl=62 time=136 ms
64 bytes from dildano.hawaga.org.uk: icmp_seq=2 ttl=62 time=132 ms
64 bytes from dildano.hawaga.org.uk: icmp_seq=3 ttl=62 time=132 ms

--- dildano.hawaga.org.uk ping statistics ---
3 packets transmitted, 3 received, 0% packet loss, time 2000ms
rtt min/avg/max/mdev = 132.002/133.335/136.002/1.931 ms

easy peasy. shame it's quite unreliable.

building an analytic engine: plan 28

2011-01-13T13:07:00.000Z

A while ago, I pledged some money to plan 28 through pledgebank.

In short:

Plan 28 is asking 10,000 people to pledge money towards building the Analytical Engine

It sounds like the project is going to go ahead even though they haven't reached the 10000 people they wanted. But maybe you want to make a pledge anyway?

3d cat

2011-01-09T11:30:00.001Z

here is a picture of me with a stuffed cat at the oxford natural history museum. I happened to have two frames with a slight difference in position, so I combined them in an animated gif in a 3d display technique that I've seen before. It has the advantage that you don't need special viewing apparatus, but the disadvantage that you get seasick watching it.

pool.ntp.org

2011-01-02T10:06:00.005Z

I've used pool.ntp.org to give me reasonable NTP servers before. On Christmas day I investigated how I could add my server. It turns out there is a self-service user interface to do so, with a scoring system that dynamically decides if your server is good enough to be published.

So I added by NTP server ntp.hawaga.org.uk (that also does a bunch of other stuff), waited a while for the score to rise, and then sat back and watched the port 123 packets flow.

There is lots of fun stuff about NTP breaking in ways which result in server floods - summarised in Wikipedia's NTP_server_misuse_and_abuse

One accusation that I've seen is that 50% of traffic is well behaved clients, and that the other 50% is a small number of misbehaving hosts which poll and poll and poll and poll. I've seen that behaviour in some of my tcpdump runs, though that is not too bad today:

Over a 15 minute period, I got 282 packets, less that one per second, from 53 different IP addresses, with a very unbalanced distribution: 24 hosts sending one packet, 50 sending less than one per minute (15 packets total), 3 sending more than one per minute, and one host sent 65 packets.

Update (Jan 6th 2011): You can watch the score history for my server in my pool.ntp.org profile, although at time of writing its kinda dull, being a flat top score for the past few days.

Update (Jan 7th 2011): I grabbed packets for about the last 24, and see 2736 distinct IP addresses, 32778 packets total (8 packets avg), noisiest host was 85.248.56.73 with 4628 packets. Anyway that's the most number of users I've ever provided service to, I think!

Update (Jan 17th 2011): I now have MRTG monitoring this server's estimated offset from correct time (similar but different to the profile graph above):

cybersyn

2010-12-26T13:45:00.001Z

I found this in wikipedia:

Project Cybersyn was a Chilean attempt at real-time computer-controlled planned economy in the years 1970–1973 (during the government of president Salvador Allende). It was essentially a network of telex machines that linked factories with a single computer centre in Santiago, which controlled them using principles of cybernetics.

I think that's quite an interesting cross-over between socialism and computer control.

The wikipedia page has a cool pic of the "control room" which looks totally Star Trek (although other reading suggests that was a prototype control room and not actually used in real life).

latex double-cite

2010-12-19T13:57:00.000Z

Turns out LaTeX you can write markup like


\cite{a,b}

to get multiple citations in the same place like this: [1,2]

Which is kinda obvious.

But I'd never thought of it.

foreign sim cards work better

2010-09-26T14:52:00.000+01:00

international mobile phone roaming has a strange property: in any particular location, a foreign roaming sim card gets better coverage rather than a local sim card: generally all local networks are available for a foreign sim card to connect to, but only one network is available for the local network.

extreme diving for work

2010-09-12T17:36:00.000+01:00

Some quotes from a paper on the Reduced Gradient Bubble Model for scuba diving decompression calculation which I've been looking at recently. Most of what I've looked at so far has been recreational no-decompression diving, so the dives described below seem quite extreme. (for comparison, the deepest recreational dives are to about 40 metres = 130 feet, and for a maximum of 8 minutes)

Pearling ﬂeets, operating in the deep tidal waters off northern Australia, employed Okinawan divers who regularly journeyed to depths of 300 f sw for as long as one hour, two times a day, six days per week, and ten months out of the year.
[...]
With higher incidence of surface decompression sickness, as might be expected, the Australians devised a simple, but very effective, in-water recompression procedure. The stricken diver is taken back down to 30 fsw on oxygen for roughly 30 minutes in mild cases, or 60 minutes in severe cases. Increased pressures help to constrict bubbles, while breathing pure oxygen maximizes inert gas washout (elimination).

Similar schedules and procedures have evolved in Hawaii, among diving ﬁshermen [...] Harvesting the oceans for food and proﬁt, Hawaiian divers make beween 8 and 12 dives a day to depths beyond 350fsw.
[...]
Consistent with bubble and nucleation theory, these divers make their
deep dive ﬁrst, followed by shallower excursions.
[...]
In a broad sense, the ﬁnal shallow dives have been tagged as prolonged safety stops.

new photo frame

2010-09-05T14:12:00.000+01:00

On sale, €33 at Media Markt, I got a digital photo frame.

It has a slot for a USB stick, and for various memory cards. It looks like an upgraded version of one I bought for my parents a year ago, where the USB interface worked well but the card reader seemed unreliable. So I put one of the many free conference USB sticks in my collection in.

People seem to have an instinct to unplug these things continuously. Why? You don't put curtains over the print photos on your wall and only open the curtains for a few minutes at a time to look at the photos behind.

The frame is 16:9 aspect ratio. My camera makes files of ratio 4:3 (or 3:4 in landscape). (apparently print photos are usually 3:2. my camera has a helper mode that overlays grey bars on screen to show you 3:2 ratio. But it doesn't have a similar mode for 16:9)

On my laptop, I have gimp. But I found that Preview is good enough for rough cropping of photos to size. That's the technical side of cropping easily dealt with. On the artistic side, though, its hard to get in the habit of evaluating photos for such cropping - photos that I think of as "too much space at the top / bottom" are ones that are perfect for this frame, and photos that fill the frame nicely are too full for cropping.

As the frame is so low resolution (~ VGA) its possibly to crop smaller details from a frame, so that you end up with an entirely new picture rather than something that looks like the original photo but a bit cropped.

I've had a desire but not enough motivation to actually look at my photos from a cropping perspective. Perhaps this will provide the motivation.

nominal, ordinal, interval, ratio

2010-08-29T01:31:00.002+01:00

Decision by Objectives (DBO) classes applications of numbers into a hierarchy of four different types, each building on the properties of the previous one.

The concepts are not unfamiliar at all to a mathematician, but they are approaching from a management direction rather than from pure mathematics, and I think that is an interesting different perspective.

The first application of numbers is nominal. In this application, numbers are used to name things. DBO gives examples from horse racing: The number on a jockey or a horse is a nominal use. It identifies a particular jockey or horse; but it is meaningless to (for example) add two jockey numbers together, or divide one by another. In Maths, that means it is possible to permute the numbers in any way without losing any information. The numbers, ℕ, are used purely as a set of distinct objects without structure or relation. We could equally well use any other sufficiently large set of symbols (such as letters).

The next application of numbers is ordinal. In this application, numbers are used to order things. In the horse racing example, the finishing order of the horses is an ordinal application. Some horse finishes first, another finishes second, yet another finishes third. In Maths, there is a linear order between the numbers, and we have a relation < or ≤ that makes sense. We can compare numbers in this application, with a notion of bigger or faster or stronger). But it still doesn't make sense to (for example) add or subtract those numbers, or to make statements like "horse X finished 3 places ahead of horse y".

The third application of numbers is interval. It makes sense to subtract interval numbers from each other. The authors are a little vague in DSO about whether they think it makes sense to add interval numbers. I think in some applications it does (how much chocolate did you eat? how much chocolate did I eat? we can compute: how much chocolate did we eat together?) but in some it does not (what is the time now? what time did the meeting start? we can compute: how long has the meeting been going on (subtraction), but adding the time now and the meeting start time doesn't make sense). When it does make sense to add, the numbers form a group with operation +. When it only makes sense to take the difference, then the numbers form something like a torsor - a group without identity.

The final application is ratio. These is use of numbers where ratios make sense - for example, a horse might finish in half the time of another, meaning that the ratio of the time of the first horse to the second horse is 1/2. It makes sense to multiply and divide these numbers; and ratios can also be used to scale interval numbers. Mathematically, we have a (meaningful use of a) field, ℝ or ℚ.

The point of them making these distinctions in DSO was to point out that just because you have some information in your decision making represented as numbers, it doesn't always make sense to do things like taking the mean, or summing, or whatever.

rsync --fake-super

2010-08-22T13:58:00.000+01:00

Every now and then I discover new options on old utilities.

One I am very happy to have discovered in rsync is the --fake-super option.

Scenario:

I have machine A. I want to back up (some portion of) the file system onto machine B. I want to include permissions and ownership (for example, because I am backing up /home.

I can run rsync on machine A as root from a cron job. OK. But then (traditionally) it needs root access to machine B in order to set permissions and ownersip of the files it creates. I can't have it connect to machine B as some normal user because of that. Additionally, the user-id and group-id name/number spaces on both machines need to match up somewhat so that users on machine B don't get access to files they shouldn't have access to.

--fake-super changes that. When rsync tries to change the permission or ownership of a file and finds that it cannot do that, it instead stores that information in extended attributes on that file. So now access to machine B can be through some normal user account without special privileges.

A downside is that if some user has an account on both sides, they don't get full privilege access to the backups of their own files.

Another use I found for this is on my laptop under OS X, where one of my external hard-drives is now mounted with an option to prevent user and group IDs being changed, or makes them ignored somehow (presumably for a better experience when using the hard-drive on multiple machines).
Incremental rsync backups were experience an inability to change group ownership on files, which mean that instead of being hard-linked (using --link-dest) they were being copied afresh each time. This was fixed by --fake-super too - instead of changing ownership on the external HD filesystem, they're added to the extended attributes.

fractions and proof-irrelevance IV - forgetting proofs

2010-08-18T12:21:00.000+01:00

Continuing from previous posts on implementing fractions in Agda.

We've tried to force our representations of fractions to have a canonical form, but requiring the inclusion of a proof of that canonical form breaks canonicity.

So we need a different approach.

Data.Rational does it something like this, which I found hard to understand at first. Trying to understand isCoprime here was the motivation for this sequence of posts:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : True (coprime? ( ∣ numerator ∣ ) (suc denominator-1))

isComprime is different. Rather than directly expressing a proposition (Coprime numerator (suc denominator-1)) as the type of isCoprime, we instead use a slightly different proposition (coprime?) and wrap it in True.

coprime? has type Decidable Coprime. It is a decidable version of the coprime proposition. A normal proposition type has values that are proofs of that proposition. If I give you a proof, then you know the proposition is true. However, if I don't give you a proof, you don't know that the proposition is false. Perhaps its true but I haven't given you a proof. A decidable proposition type has values that are either proofs that the proposition is true, or proofs that the proposition is false, wrapped in yes or no respectively. coprime? is a function that decide whether two numbers are coprime or not, and return a corresponding proof.

True is a function that maps a decidable proposition type into another type: either ⊤ (when the proposition is true) or ⊥ (when the proposition is false).

⊤ (top) is the unit type, that has only one member value. ⊥ (bottom) is the empty type with no member values at all.

Both of those seem a bit useless to a traditional programmer: if I have a variable of the unit type ⊤, it can only have one value. So then I'll always know what that value is - its pretty much a constant. So why have a variable? And if I have a variable of the empty type ⊥ then I can't ever invent a value. If that variable is an input parameter, I can never even call my program, because I can't give input parameters. But it turns out this weird behaviour is exactly right for Data.Rational.

Say I'm going to construct a half. I'm going to pass numerator = 1 and denominator = 2. We also need to pass an isCoprime parameter.

To start with, what type of parameter is that?

That depends on the value of numerator and denominator (that's what dependent types are). Once we know the numerator and denominator, we can evaluate the expression True (coprime? ( ∣ numerator ∣ ) (suc denominator-1)) to find out the type of isCoprime. 1 and 2 are coprime, so coprime? evaluates to yes _, and so True (yes _) evaluates to ⊤.

So we need to give a value for coprime that is of type ⊤. ⊤ only has one value, so thats the value that we'll put in isCoprime. The resulting structure has no proof of coprimality in it. If two fractions have the same numerator and denominator, then they'll always have the same value of isCoprime. So we've got equality of equivalent fractions!

But now what happens if we try to construct a non-canonical fraction, for example 3/6 ?
Once we have specified a numerator of 3 and a denominator of 6, we can figure out the type of isCoprime. 3 and 6 are not coprime, and True (no _) will return ⊥.
So we need to provide a value of type ⊥. There are no values in ⊥. So there is no way we can call the constructor in this case, because we can't come up with a value for each parameter.

So now the goal is achieved - a data structure for representing rationals, where equal rationals are definitionally equal.

My goal in picking apart Data.Rational like this was two-fold: i) I wanted to use rationals, and wanted to understand what was going on; ii) I want to implement my own canonical forms (for finitely-generated abelian groups) and understanding how its done for rationals seems like a step in the right direction.

fractions and proof-irrelevance III - proofs are too isomorphic to values

2010-08-18T12:19:00.001+01:00

Continuing from my earlier post about fractions and proof-irrelevance...

In the previous post, we added a parameter to the rational constructor to require the numerator and denominator of rationals to be coprime, in order that we can only construct canonical rationals, so that we get equality that behaves "right" - when two fractions are the same, they will be equal in the eyes of Agda.

But the way we did it doesn't work quite right:

The Curry-Howard correspondence connects propositions and proofs on one side, and datatypes/sets and values/elements of sets on the other side:

Side A	Side B
	Programmer view	Maths view
Proposition	Data type	Set
Proof	Value	Element

When we added the coprimality test to the rational constructor, we added a parameter of type Coprime numerator denominator. That corresponds to the proposition that the numerator and denominator are coprime. Its a parameter so it will have a value when it is used to construct some rational, and that value will be a proof that the numerator and denominator are co-prime.

So now think about constructing a half. We'll put in numerator 1, and denominator 2, and some proof, pr1, that {1,2} are co-prime.

Now somebody else builds a half. They'll put in numerator 1, and denominator 2, and some proof, pr2, that {1,2} are co-prime.

Now I'm going to compare my half to that other person's half to see if they are equal. They're equal if all the constructor parameters are equal. The numerator, 1, matches. The denominator, 2, matches. But we have a third parameter now, the coprimality proof. Do they match? Does pr1 = pr2 ? In general, no, that isn't the case. There could be many different proofs of the same proposition.

So we've ended up with a canonical form for the numerator and denominator, but we've just pushed the problem into a different field of the data structure, and we still don't have a canonical data structure.

Somehow we want to insist that the coprime proposition is true, but without different proofs of that causing different representations of fractions. That is proof irrelevance.

Read on for part IV, the final part

fractions and proof-irrelevance II - equality of fractions

2010-08-18T12:18:00.001+01:00

This continues from the first in a series of posts reviewing the implementation of Data.Rational in Agda.

We've got a datatype for representing fractions, ensuring that the denominator is strictly positive. So now any element of the mathematical set ℚ can be represented by an element in our datatype ℚ; and vice-versa any element of our datatype ℚ represents an element of the mathematical set ℚ.

Sometimes, we want to be able to compare fractions to see if they are the same or not. It's fairly straightforward to define an equivalence relation between two fractions, using integer multiplication, something like this:

p ≃ q  =  P.numerator ℤ* Q.denominator ≡ Q.numerator ℤ* P.denominator

But sometimes we want to use equivalence where we don't get to specify the equivalence relation. One example of that is type-checking: say we want to use a fraction (for some purpose) as part of a type specification. In that case, we need equivalent fractions to be definitionally equal: they must have been constructed with the same constructor, and the parameters to the constructor must be the same.

The numerator, denominator representation described in the previous post breaks down here: we can represent a half as numerator = 1, denominator = 2; but equally well as numerator = 3, denominator = 6. Yet, 1 ≠ 3 and 2 ≠ 6 so the two representations are not definitionally equal.

One way of solving this is by forcing the representations to be in some canonical form. For fractions, one such form is when the numerator and denominator are co-prime so that there are no shared factors. This way, 1/2 is the canonical representation of a half. 3/6 = (3*1) / (3*2) is not, because 3 is a factor of both the numerator and denominator.

So maybe we could demand that when you call the constructor for a fraction, you have to prove that the numerator and denominator are co-prime, by defining something like this:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ
    isCoprime     : Coprime ( | numerator | ) (suc denominator-1)

That way, whenever we construct an element of ℚ, we'll know that the numerator and denominator are co-prime, because we give a proof of the proposition "Coprime numerator denominator" (see that we would add one onto denominator-1 to get the denominator).

Read on for part III...

fractions and proof-irrelevance I - sane denominators

2010-08-18T12:17:00.001+01:00

This begins a series of posts reviewing the implementation of rationals in Agda.

I'll talk about broken ways of building the rationals ℚ in Agda, how its desirable to be able to compare rationals for equality, how having proofs in the language can get in the way of that, and how to cope with that.

This is all based on the code I found in the Data.Rational standard library module, which I have been trying to understand as I want to use both the module itself, and its techniques, in a scientific units-of-measurement library that I am writing.

Rationals

A rational (or a fraction) can be described as an integer (the numerator) divided by a strictly positive integer (the denominator).

It's not hard to build an Agda data type to represent a fraction as a pair of two integers:

data ℚ : Set where
    field
      numerator : ℤ
      denominator : ℤ

This implemenation doesn't require the denominator to be a positive integer, though. So we can represent "invalid" fractions. Most importantly, we can represent a fraction with denominator 0 this way, which is nonsensical.

So lets store the denominator minus 1 as a natural number (0, 1, 2, ...) like this:

record ℚ : Set where
  field
    numerator     : ℤ
    denominator-1 : ℕ

The denominator minus 1 can be 0 or higher, which means the denominator can be 1 or higher - a positive integer as desired.

On the downside, now every time we want to compute with the denominator, we have to compute it first by adding one to the denominator minus 1.

This is a pattern I found strange (and still find unintuitive) in Agda. Rather than storing something in a format that you want (the denominator), you instead store it in a format that makes correctness work.

Read on for part II...

acetate slides

2010-08-15T11:27:00.000+01:00

This pdf shows an interesting style of PDF slide generation that seems to be "acetates + digital camera". I guess they were presented on acetates to begin with and scanned in? Not so weird as I first though, which was that they were drawn on whiteboard and photographed... but still novel compared to powerpoint.

Erdős number

2010-08-08T12:09:00.001+01:00

There's this concept of an Erdős number for an academic author: take the graph of academic authors where two authors are joined together if they have written a paper together; then your Erdős number is the number of hops from you to the currently deceased mathematician Paul Erdős.

I first read about him a decade ago in The Man Who Loved Only Numbers but I've never got round to actually computing my number 'till now.

Borja Sotomayor shares a co-author with me (Ian Foster), so my number is less than or equal to his. He is number 6, so my number is ≤6, through this chain:

Ben Clifford → Ian T. Foster → Patrick H. Worley → Robert S. Schreiber → John Russell Gilbert → Roger C. Entringer → Paul Erdös

(p.s. its hard to type the ő in Erdős. Its not ö, although it looks like it)

weight-based electrical measurement and other fun stuff

2010-07-29T13:53:00.007+01:00

From a paper On the security economics of electricity metering by Ross Anderson and Shailendra Fuloria (via Bruce Schneier's blog), a few of quotes that amused me.

Edison invented a meter consisting of a jar holding two zinc plates: each month the electrodes were weighed and the customer billed according to the change in their weight.

and

For example, customers in Soweto noticed that their meters would set themselves to maximum credit in a brown-out (a voltage reduction to 160-180V) because they had not been tested adequately for African conditions; this only came to light when customers started throwing chains over the 11kV feeders in order to credit their meters.

and (about california):

generators had enough market power to boost peak prices by shutting down some of their plants for “maintenance reasons”. They had learned this trick in 1998 when the replacement reserve price of electricity peaked at $9,999.99/MW in July as against the average of $10/MW for the ﬁrst three months of the year

A bit later they talk about contract languages, which reminds me very much of recent talk of expressing stock market contracts in Python:

This analysis suggests a technical research project: to design a command language for meters that enables an energy company to specify complex tariﬀs in a piece of signed downloaded code that would implement a particular contract between the supplier and the customer. The sort of tariﬀ we have in mind is: “Your basic rate is 5p from midnight to 0600, 15p for the peak from 1730 to 2100 and 10p the rest of the time; however the 15p basic peak rate applies only provided you restrict demand to two kilowatts else it becomes 50p. Furthermore we may at any time request you to limit consumption to 1kW and if you don’t then any half-hour segment during which you draw more than 1kW at any time will be charged at 50p”. The code would have to export to the energy company enough data for it to bill the customer correctly, and enough to the distibution company for it to operate the system eﬃciently. This problem is nontrivial but we believe it is solvable.

branching on the left vs branching on the right (agda bubble sort part 3)

2010-07-23T17:38:00.001+01:00

I gave a definition of onepass, the inner loop of my Agda bubblesort implementation, in an earlier post.

That wasn't the first implementation that I tried.

Instead, first I wrote it like this, in a way that uses with expressions. The difference is that the version I wrote uses an if construct that is manually defined. Agda seems to prefer doing case analysis / branching using with, which makes it seem as if you're getting a new parameter to pattern match on - in the below example, the results of y ≤? y which is either yes _ or no _.

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) with y ≤? y'
  ... | yes _ = y :: (onepass {suc n} (y' :: y0))
  ... | no _ = y' :: (onepass {suc n} (y :: y0))

For comparison, here's the definition in my first post:

onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then        
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0))

The two implementations do the same thing at runtime - they swap the first two elements of the list and recurse. But their compile-time behaviour is different.

The with-based version doesn't pass the termination checker. The if-based one does.

The with-based version with with the proofs that I gave in part 2. The if based version doesn't.

So I pretty much am forced to choose: I can use the with-based definition, and turn off the termination checker in the Agda compiler. Or not. Either way seems pretty lame. In order to proof all this stuff, I have to turn off the termination checker which is a key part of checking the proofs that I'm writing.

I don't really understand what is going on inside Agda to make the first version not work. But that's what I actually use in practice (with termination checking turned off) - perhaps I can investigate a bit more later. But for now, I want to continue working on a proof (albeit not termination checked) that bubblesort actually sorts...

permutations (bubble sort in agda, pt 2)

2010-07-22T14:04:00.000+01:00

(following from part 1)

I implemented bubblesort in Agda, and it looks bug-free. But I want to prove that it is correct. First I want to prove that the output is a permutation of the input. I'm not going to try proving anything about the ordering yet, but I want to know that at least I'm getting back the same list, rearranged.

This is where Agda starts getting really hard for me, and becomes more like stuff I did in my maths degree courses than stuff I've done with hobby computer hacking. Except you can't write "clearly, .... is true" in your Agda programs like you could in your maths homework, so you don't get to bluff your way through proofs quite so easily.

The previous post showed how you could augment the datatypes of the functions in your program to carry more information about how those functions behave. That's one way of using dependent types. In this post, I'm going to use a different style to prove that the output of bubblesort is a permutation.

The Curry-Howard isomorphism which (for the purposes of this post) says (for the purposes of this post) that you can regard propositions as types, and proofs of those propositions as values in those types.

So you define a type to represent whatever proposition it is you want to prove, and then you write a function that creates a value of that type - that value is then a proof of the proposition. When you use values normally, you care what that value is. When you use proofs though, you don't care so much what the proof is. You just care that the proof exists.

First I need to make a definition of what I mean by permutation. There are a few different ways I could have done this. I ended up settling on this one:

data SwapBasedPermutation {A : Set} : {n : ℕ} -> (Vec A n) -> (Vec A n) -> Set where

    reflexivity : {n : ℕ} -> (i : Vec A n) -> SwapBasedPermutation i i

    transitivity : {n : ℕ} -> {a : Vec A n} -> {b : Vec A n} -> {c : Vec A n} -> (SwapBasedPermutation a b) -> (SwapBasedPermutation b c) -> SwapBasedPermutation a c

    prepend : {pn : ℕ} -> {l r : Vec A pn } -> (e : A) -> (SwapBasedPermutation l r) -> SwapBasedPermutation (e :: l) (e :: r)

    swapheads : {pn : ℕ} -> {first second : A} -> {rest : Vec A pn} -> SwapBasedPermutation ( first :: second :: rest ) ( second :: first :: rest)

My permutations are swap-based. Given a list, you can swap the first two elements (using the swapheads constructor, and you get a proof that the first list (but only the first two elements, not some arbitrary pair of elements) is a permutation of the second; and given two lists that are permutations of each other, you can add the same element onto the front of both, and you get a proof that those two new lists will be permutations of each other (using the prepend constructor).

I also declare that permutations are reflexive and transitivitive by definition (although I think I could build those up from more fundamental parts, but I'm more interested in looking at the higher level behaviour of bubblesort).

Those are proofs-by-definition and so they are trivially true (at least as far as the type-checker is concerned).

Now given this SwapBasedPermutation type, I can write a theorem that the top level sortlist function (defined in my previous post) outputs a permutation of its input.

The theorem is a type signature for a function, and body of the function needs to generate a proof of that theorem:

The type signature for my theorem looks like this:

sortlist-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (sortlist l)

It says: for all ℕumbers n: for all Vectors l of length n: l is a permutation of sortlist l.

If we can write a definition for this function that typechecks correctly, then this theorem holds. We never actually need to invoke the function at runtime - it is enough to know that we could. (That's another thing thats a bit weird in Agda- you're writing functions that will never be called at runtime but they're still useful. I guess its like writing javadocs...)

Here its important that Agda functions are total - we need to know that our proof generating function really will return a value and not loop forever or error out. Otherwise, our theorem could typecheck but not really be proved.

Now that we've stated the theorem (as a type), we need to build the body (the proof).

To get there, we can define lemmas, in the same way that you can define helper functions to help implement your main function.

First, invoking onepass on a list permutes that list. onepass is the code in my implementation that actually re-orders the list, so the proof of this lemma makes use of the swaphead definition. It also recursively calls itself on a smaller list - that means we're using proof by induction. This definition roughly follows the shape of the definition of onepass itself.

lemma-onepass-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (onepass l)
  lemma-onepass-permutes [] = reflexivity []
  lemma-onepass-permutes (e :: []) = reflexivity (e :: [])
  lemma-onepass-permutes (y :: y' :: rest) with  y ≤? y'
  ... | yes _ = prepend y (lemma-onepass-permutes (y' :: rest))
  ... | no _ = let                      
       p1 = lemma-onepass-permutes (y :: rest)                              
       p2 = prepend y' p1
       p3 = swapheads -- magically the list that we're swapping the             
                      -- heads for is inferred (from use in p4)                 
       p4 = transitivity p3 p2
    in p4

Another lemma, this time about the behaviour of innersort:

lemma-innersort-permutes : {vn : ℕ } -> (sn : ℕ) -> (l : Vec ℕ vn) -> SwapBasedPermutation l (innersort sn l)
  lemma-innersort-permutes zero l = reflexivity l
  lemma-innersort-permutes (suc sm) l = let
             a = lemma-onepass-permutes l
                  -- this shows l is a permutation of onepass l                                  
             b = lemma-innersort-permutes sm (onepass l)
                  -- this shows that (onepass l) is a permutation of (innersort sm (onepass l))               
          in transitivity a b

and finally we can give our definition for our theorem, sortlist-permutes, using these lemmas:

sortlist-permutes {n} l = lemma-innersort-permutes  n l

And now, because sortlist-permutes typechecks correctly at compile time, I know that I can generate a proof that sortlist really does permute a list, no matter what list I give it.

Tada!

Except this doesn't actually typecheck in Agda due to a problem with my definition of onepass... see the next post.

bubblesort in agda (part 1)

2010-07-21T20:20:00.003+01:00

I've been playing with Agda, a dependently typed programming language (where types of expressions can depend on earlier values).

Dependent types let you make quite rich compile-time assertions about the behaviour of your program. These assertions are written and checked using the type system.

One of the examples for Agda seems to be quicksort. So, I thought I'd experiment with bubblesort - similar but different.

First I want an implementation of bubblesort in Agda. Then I want to use dependent types to express something interesting that I cannot express in another language: that bubblesort really sorts.

Agda looks syntactically quite like Haskell, so I first made a Haskell implementation. This doesn't look like a procedural normal bubblesort implementation, as I wanted to keep a functional style.

bubblesort t = applyLoop t

applyLoop t = if isSorted t then t else applyLoop (onePass t)

onePass [e] = [e]
onePass t =
  let a:b:rest = t
      (as,bs) = if a < b then (a,b) else (b,a)
      newlist = as:bs:rest  -- list with head two elements in order
      bsrest = onePass (bs:rest)
      endlist = as:bsrest
    in endlist

Next I wanted to convert the above Haskell code into Agda. Syntactically, this translates quite easily.

My only major stumbling block comes with termination.

Functions in Agda must be total.

That means they must always terminate with a value. They can't fail with an error, and they can't run forever (which means that Agda is not a turing-complete language, I think!)

Agda contains a termination checker that gives a compile error if it can't prove that your functions terminate.

Bubblesort does always terminate. But the Agda compiler can't see that from the above definition. The proof looks something like: every iteration of applyLoop makes the list more sorted, and once you've called it enough times (as many as there are elements in the list) then the list will be sorted.

So I changed my implementation to run the outer loop a fixed number of times, rather than until the list is sorted. That makes the termination provable. But it makes it less obvious that the final result is actually sorted: now we end after a certain number of runs, rather than when the isSorted test is true...

Here's the Agda code:

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then                   
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0)) 

  innersort : {n : ℕ} -> ℕ -> Vec ℕ n -> Vec ℕ n
  innersort zero list = list
  innersort (suc i) sorted = innersort i (onepass sorted)

  sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n
  sortlist {n} l = innersort n l

(I actually started with a different definition of onepass - I'll come back to that in a different post).

Now, that's enough (given wrappers for main, etc) to successfully sort a list:

$ ./run
2 :: 3 :: 5 :: 8 :: 11 :: 12 :: 14 :: []

So what's different from doing this in Haskell?

Well, on the downside, it is not as obvious that this sort actually returns a sorted list, as mentioned above.

On the upside: we know that this program won't loop forever (although it might loop for a very long time) - because of the termination checker.

And the types of the functions, which I haven't mentioned yet, tell us something that relates the inputs and the outputs. sortlist has a type that tells us that its output will be the same length as its input. This is not a full definition of sortedness but its more than is offered by Haskell lists.

The type signature looks like this:

sortlist : {n : ℕ} -> Vec ℕ n -> Vec ℕ n

which says something like: sortlist is defined for every natural number n, and takes as input a Vector (of ℕumbers) of length n and returns as output a Vector (of ℕumbers) of that same length n.

The type checker checks that this is true at compile time, so the inner functions must have the length similarly encoded in their types.

At compile time, when we call n, we don't know what the n will be for every invocation (this is not Pascal statically-sized arrays) - but we do know that the output will be the same size as the input.

Compare that to type of the Haskell implementation:

bubblesort :: [Int] -> [Int]

which says that bubblesort takes a list of numbers and returns a list of numbers. Typewise, a perfectly valid implementation of quicksort here could return the empty list [] for every input. This can't happen here.

So in subsequent posts, I want to try to make compile-time assertions richer. I want to prove that bubblesort really sorts, by which I mean (I think):the output is a permutation of the input; and the output is in order.

(note 1) actually the Haskell type is: bubblesort :: (Ord t) => [t] -> [t] meaning Lists of anything that can be ordered, rather than lists of integers. That same abstraction is mostly achievable in Agda, but not quite - it doesn't have typeclasses in the same way that Haskell does.

Read part 2...

autoconf and portable programs: the joke

2010-07-15T10:23:00.000+01:00

This is not my rant, but I like it:

I have a simple request for you: each time you run into software that does
this idiotic kind of test, please interact with the idiots upstream for
whom all the world is linux, and try to get them to replace their "joke"
of an autoconf macro with actual genuine tests that actually CHECK FOR THE
FUCKING FEATURE.

http://marc.info/?l=openbsd-ports&m=126805847322995&w=2

chess rankings for photos

2010-07-03T11:24:00.000+01:00

I have a lot of photos - around 50000. I want to have some kind of scoring system for them.

The obvious one is something like a 5-star scale: when presented with a photo, you can award it from 0 to 5 stars, with 5 being best and 0 being worst.

But thats not very granular, and it is not clear to me that clearly defined standards for the 6 different scores will emerge.

I preferred something that says "this is better than that, so this should have a higher score than that".

But I don't want to have to manually make a strict linear order of all photos (despite the fact that a numerical score would do so), and I want the system to tolerate inconsistencies (eg. A>B, B>C, C>A) somehow.

Eventually I read about chess ranking, where each player is assigned a numerical score indicating their "goodness" and the scores are adjusted by pairwise comparisons between players - chess matches.

I adapted this for scoring my photographs. I started with the glicko system and modified it some.

The way this works is:

Photos compete against each other, as chess players compete against each other. The equivalent of a chess match is a presentation of two photos alongside each other in a web browser, with the user clicking on the photo they prefer. So, users do not assign an absolute score to a photo. Nor do they pick how much better one photo is than the other. They pick have a simple choice: "a>b" or "b>a".

Each photo is assumed to have a single numeric score, such that the difference in the score reflects the probability that one photo will win over the other photo. (this is affine: 900 vs 1000 is the same probability as 4000 vs 4100)

It is assumed that the score cannot be known exactly, but is approximated by a normal distribution (so there is a mean, and a standard deviation).

Adding a comparison between two photos gives information about the distributions for both photos causing the mean and standard deviation to be changed to more accurately reflect the score, as described in the glicko paper.

For my 50000 photos from the past 5 years, I have about 20% voted on at least once.

For a recent trip to rome, where I took about 1000 photos, it took a few hours to include each photo in at least one vote, where each comparison was an unvoted photo vs a random photo (which may or may not have been previously voted). This does not give a huge amount of information per photo.
Once that was done, I spent some hours making other votes: sometimes random vs random, sometimes random vs the photo with the closest mean. This caused rankings to become somewhat refined (sometimes causing surprisingly large changes in mean score)

So here are the top 3 photos from that trip:

and here are the bottom 3:

It seems to work reasonably well, though I think I need many more votes to get more accuracy. But that will come over time: as new photos are added, they'll get their scores by being compared against old photos, which will give more information about the old photos too.

normally distributed random numbers in haskell

2010-06-19T01:48:00.000+01:00

somehow I expected to be able to get a normally distributed random number in haskell really easily by typing some term like "haskell random normal" into google. that came up with a bunch of stuff but nothing so simple as:

n <- getNormal mean dev

.

The most promising seemed to be the cabal package random-fu - although it looks like it has a lot of stuff in it and really all I want is the above single monadic action.

Cue the usual BS about installing packages (not haskell specific, just damned packaging in general) - today I need to edit my local hackage repository to remove some malformed packages, and upgrade GHC. frr. 6 hours just getting cabal install random-fu to work.

But once that was all done, the next morning, I got what I wanted - a short IO Double action: sampleFrom DevURandom (normal mean dev)

Hurrah.

rlwrap

2010-06-12T09:37:00.001+01:00

I got frustrated when some application I was using *still* didn't support delete properly and discovered that the solution in that community (the OCaML world) seems to be (at least for commandline use) to use 'rlwrap' to add readline support to arbitrary applications.

eg:

$ rlwrap cat
Now you can use readline features (eg delete, cursor movement) to edit text

Neat.

http://utopia.knoware.nl/~hlub/rlwrap/

pink panther usb hub

2010-06-05T00:01:00.000+01:00

I got this pink panther USB hub from mediamarkt - it was the same price as a USB extension cable (which is what I was looking for) - €7.99

Now I have three extra USB ports too, which is useful for attaching (for example) bamboo encrusted memory sticks, or my wide SD card reader.

One problem: when there are two of them chained with my ext hd on the end, the ext hd makes terrible clicking sound and doesn't start up properly. maybe thats a power problem?

64 bit linux BS

2010-05-28T15:46:00.000+01:00

Several years ago I shied away from using 64-bit linux because many programs seem to have obscure bugs related to that. Its frustrating that I am still to this day encountering such bugs.

For reasons which might not be intuitively obvious, the broken behavior is required

2010-05-21T00:01:00.000+01:00

I previously regarded /usr/bin/env as being portable onto any sane unix platform.

But now I've had to work with FreeBSD and my beliefs are dashed.

FreeBSD /usr/bin/env implements what posix says, rather than what everyone else does. That leads to trouble when you want to pass a parameter in a shebang, like this: #!/usr/bin/env perl -w which works almost everywhere but not in FreeBSD :(

monads: overloading semicolon, && and ||

2010-05-15T00:01:00.000+01:00

Monads are sometimes described as 'overloading semicolon', aimed at eg. the C or Java programmer. This is some text about that idea.

But references there don't seem to refer to && and || - two other control operators that are regularly used (especially in C) and that I think are interesting to compare to ;

&& and || are defined primarily as 'boolean or' and 'boolean and'. But its very common to write expressions like this:

succeeded = (p != NULL && *p==5)

Evaluation of this uses more than the 'boolean and' functionality of &&. It also uses the property that && only evaluates its second parameter if its first parameter returned true - if the first parameter returned false, then the second parameter is never evaluated. That's a little bit of laziness sneaking into an otherwise strict language. In the example above, it stops the evaluation of *p when p is a null pointer.

So contrast ; and &&.

If you're a C programmer, they're totally different things - ; sequences statements, and && is an operator. Try to forget that difference for now.

You can write:

f() ; g()

which executes f, discards its result and then executes g.

Or you can write:

f() && g()

which executes f, then if f does not fail, it executes g - if either f or g fail then the expression as a whole fails, otherwise the expression succeeds. What do I mean by fail? I mean that f and g must return booleans indicated whether they succeeded or failed at doing whatever it was they were supposed to do.

So there are different ways to sequence operations (; and &&, and the operations (f and g) need to have different interfaces depending on the particular way of sequencing: when using ; there are no particular constraints. When using && we must indicate success or failure in every operation.

Both of these look like the Haskell operator >>: In Haskell, you can write:

f >> g

meaning "first do f, and then do g". But the novelty is that >> has different meanings in different contexts - and those contexts are called monads.

For example, the IO monad behaves quite like ;

print "hello" >> print "World"
hello
World

which looks like:

printf("hello\n") ; printf("world\n");

and the Maybe monad behaves a bit like (but also a bit different from) &&

main() {
 test() && printf("world\n");
}

int test() {
  return (2==3); // fail...
}

prints nothing.

In Haskell, the Maybe monad looks more like this:

Nothing >> Just 5
Nothing
Just 1 >> Just 5
Just 5
Just 1 >> Nothing
Nothing

In the Haskell example, Nothing means failure, and Just something means success (more on that in a bit).

In the first Maybe expression, Nothing >> Just 5, our first statement fails, so we don't run the second.

In the second example, Just 1 >> Just 5, the first statement succeeds (it returns Just something - so then we run the second statement which also succeeds (because it returns Just something) and so the statement as a whole succeeds.

And in the third example, the first statement succeeds, but second one fails, so the whole expression fails.

To add confusion, there are two distinct syntaxes in Haskell for writing monadic expressions. They do the same thing, and there is no real advantage to one over the other so far, but in a bit, the differences will be exposed. The above has introduced one form, using >>. The other form looks like this, using the do keyword

do
  putStrLn "hello"
  putStrLn "world"

and

do
  Just 1
  Just 5

Those are the same as earlier example, but in a different syntax. When you write something using do notation it is automatically translated into >> notation by the compiler. For now, that is just joining the lines together and putting in >>, which is not much difference. But there will be bigger differences later.

The Maybe example looks quite contrived - and it is - because so far I haven't explained the other important part of monads, which is value binding. That's where the analogy with ; and && breaks down and you start getting into more functional programming territory.

Note that all the above examples are missing some things that are used all the time (in C, Java and Haskell): return values, and variable assignment. (in one of the examples, I used p but only to read, not to write). This is an area where Haskell can be quite different from languages like C and Java.

Now, remember how I said that depending on what you're using to sequence your statements, those statements must match a particular interface. For example, if you're using &&, then those statements must return a boolean success. Using && hides away that return value - you write f() && g() without actually mentioning or testing the return value. Instead you let && deal with it; and in the Maybe monad, you let >> deal with it, and if using do notation you just put statements in sequence on separate lines, and magically they'll stop running when one of them fails!

What happens when I want variables and return values though?

In the ; style of writing C, you can write:

x = f(); g(x)

Now we expect f to return a value, and later on in a subsequent statement, we want to be able to access that value. In this C example, we do that by assigning the return value of f() into a variable x and then when we want to pass a parameter to g, we can write x again to get that value back. People do that every day. Nothing fancy - just normal programming like you learned when you were 8 years old.

So now how does that work in C using && to sequence statements? We can't write:

( x = f() ) && g(x)

because we're already using the return value of f() to indicate success or
failure - we can't return some arbitrary value too. (and remember we're using && here to sequence our statements - you're not allowed to suddenly say "ok lets put a ; and then an if statement). Uh oh.

Well, actually sometimes in C, we do manage to return a value and indicate success/failure at the same time. For example, fopen returns a pointer to a FILE or returns a null pointer to indicate failure. So fopen is reporting two things: did it succeed? (null or not-null), and if it did succeed then we can extract some more information - the pointer to the FILE struct.

The Maybe monad in Haskell does something similar. Remember a statement in the Maybe monad above returns Nothing if the operation failed, or Just something if the operation succeeded. I coughed politely and ignored the something at the time. But now see that the something what the operation returns on success.

This is more general than the fopen NULL pointer case. The fopen style only works when your data-type has a "magic value" to indicate failure - when using pointers, NULL, or perhaps countDinosaurs() could return -1 if it failed. But this isn't always possible (for example, if I am using some xor() function then any output is possible and there is nowhere for me to indicate failure)... and it is awkward for every procedure to use its own convention.

So now consider our Maybe monad example from before (slightly rewritten):

f = Just 1
g = Nothing
f >> g

In this, f succeeds and returns 1, and g fails and so does not return a value.

Well, what can we do with that return value? Just like in other languages, we can use it in later computations.

Now, there are two ways of writing this: the do style and the >> style. The do style is most like C and Java, and the >> style looks totally different.

I'll try to explain both. Try to understand both - the do style should be pretty easy to understand because it looks (aside from which symbols are used) quite like Java. But the >> style is more "functional" and might steer your thinking into writing functional code functionally, rather than "writing C in Haskell" as the do notation leads to (or at least I find it tempts me to).

Lets look at the IO monad. This lets us have functions which do IO (something which is forbidden in plain Haskell code (for better or worse)).

I want to have a program which will read a line from stdin, and output it on stdout. In C, that might be (assuming we have a nice readline function):

x=readline();
puts(x);

So in Haskell: As building blocks, we have print, which is a command you can run in the IO monad that will output the string that you pass to it (this was used right up near the top of this article); and we have getLine which is a command you can run in the IO monad that reads in a line from stdin and returns it.

So we want to run getLine, and then we want to run putStrLn, passing in the value that we got from getLine.

First lets write it in do notation:

do
  x <- getLine
  putStrLn x

This style runs getLine and binds its return value to x. That means whenever you refer to x later on in the do block, you mean whatever value was returned by getLine. This style is very similar to C or Java - it looks like we do some computation, assign its value to a variable, and then later on use that variable.Now here's the more functional way:

getLine >>= print

This uses an operator >>=. This behaves a bit like >> in that it puts two operations in sequence. But it also wires up the return value of the first statement to be the parameter of the second statement.Now remember that >> is different for each monad. It represents that monad's particular way of sequencing operations. >>= is likewise different for each monad. In the IO monad, it sequences operations and passes their values around just like above.But what about in the Maybe monad?Here's an example. First we have an operation in the maybe monad that takes an integer and succesfully returns that integer incremented. We use Just something to indicate success, and that something is x+1 to increment our integer.

increment x = Just (x+1)

Lets use this:In do notation:

do
  v <- Just 5
  increment v

which gives us:

Just 6

or the same in >>= notation:

Just 5 >>= increment

In the do notation, you can write as many lines as you like, and similarly in the >> notation you can write as many statements as you like:

Just 5 >>= increment >>= increment >>= increment
Just 8

But the point of the Maybe monad is to handle failures nicely. So what happens if we have a failure? What do these two fragments do:

Nothing >>= increment

or equivalently:

do
  x <- Nothing
  increment x

Now >>= will behave like >> which in the Maybe monad is quite like how && behaves in C. Ignore the value passing bit of >>= and concentrate just on the >> bit of it: in the Maybe monad, >> behaves like && - if the left-hand side fails, then we don't evaluate the right hand side. And thats what happens here - the left hand side fails (by returning Nothing) and so we never even to try evaluate increment.So now look at the do notation version. First we try to bind x to some computation, but that computation fails, so we don't evaluate the rest of the line.Now look at this Java code fragment:

x = v();
 y = increment(x);

That sets x to the some value caused by running a function v, and then runs increment on that value. First we run v and then we always run increment. Right?Yes, if v looks something like:

static int v() { return 5; }

But what about this:

static int v() { throw new RuntimeException(); }

Now we evaluate v but it fails, and so we don't evaluate increment. Instead, the program as a whole fails.So now the Maybe monad looks like && but also looks like exception handling - && and exception handling are almost the same thing! (which is quite surprising sounding, but they're often used for very similar purposes).What's the difference then?Well, an Exception propagates upwards and makes the whole of your program fail, unless you explicitly catch that exception, and you use ; to separate statements.Failures with && don't propagate out of the expression using the && - instead the expression returns a boolean false to whatever program code is surrounding it, andcontinues running. Essentially, you are forced to catch the failure, because you get told explicitly "I succeeded" or "I failed" (by the expression as a whole evaluating to true or false).So, I've shown two notations for monads - do notation and >> notation - and a few examples of code written in both styles. Turns out you've already probably written code in both styles if you've programmed in C and programmed in Java, because you will have used && for error handling in some places, and Java exceptions in some other places. So there's nothing new here.Which style is better? Well, it depends...If you are passing a value from one operation to the next, with nothing else going on, then the >> style is very concise: getLine >> print - we don't waste space assigning the line to a variable only to use it immediately and then forget about it.But when there are lots of actions returning lots of values, it can be easier to use the variables of do notation to keep track of them all:

do
  print "what is your name?"
  name <- getLine
  print "what is your age?"
  age <- getLine
  print ( "Hello "++name++". You are "++age++" years old and you are cool!" )

Using >> notation is awkward here - somehow you need to combine 5 actions into a linear sequence of actions to perform: print >> getline >> print >> getline >> print but you need to wire the values from getline around in non-linear fashion.Its possible (indeed, when you write in do notation it is translated into >> form by the compiler, as I said above) but it looks ugly - its easier often to use do notation and let the compiler sort it out for you.The Maybe monad adds failure handling to sequenced operations. It turns out that you already probably used that functionality without explicitly realising that was happening. What other interesting stuff can we build by making a monad with its own >> behaviour?One that gives behaviour that you don't find natively in C or Java is backtracking and filtering computation using the list ([]) monad.In the IO monad, a monadic action always returns a value. In the Maybe monad, a monadic action either returns a value or fails. In the [] monad, a monadic action can return multiple values (or one or zero values).We can use the [] monad to try out all combinations of some sets of values. For example:

do
  x <- [1,2,3,4]
  y <- [100,1000, 1000000]
  [x * y]

gives the result:

[100,1000,1000000,200,2000,2000000,300,3000,3000000,400,4000,4000000]

This looks like a normal do block, but instead of Just and Nothing from the Maybe monad, we now specify values using []. And we can put many values inside the brackets.In this code, x will iterate over each the value of [1,2,3,4], and inside that, y will iterate over each value of [100,1000,1000000], and then we'll evaluate the value of [x*y], and then all the results for every iteration will be collected together into the output list.You can write list filters like this too:

do
  x <- [1,2,3,4,5]
  y <- if isEven x then x else []
  [y]

(assuming we've defined: isEven x = x `rem` 2 == 0)This gives [2,4] as output.And we can write searches that combine both of the above iteration and filtering. For example, say we want to find all of the pairs of digits that add to 5 (for example, 3+2 = 5, so (3,2) is a solution, but 8+1=9 so (8,1) is not a solution)We can write it like this:

do
  l <- [0,1,2,3,4,5,6,7,8,9]
  r <- [0,1,2,3,4,5,6,7,8,9]
  if l+r==5 then [(l,r)] else []

which gives us this answer:[(0,5), (1,4), (2,3), (3,2), (4,1), (5,0)]There's a more specific syntax for the list monad in Haskell, called list comprehensions. The above could be written as:

[(l,r) | l <- [0,1,2,3,4,5,6,7,8,9], r<-[0,1,2,3,4,5,6,7,8,9], l+r == 5]

To keep tying in with other langauges, Python has list comprehensions too with a very similar syntax:

>>> [(x,y) for x in [0,1,2,3,4,5,6,7,8,9] for y in [0,1,2,3,4,5,6,7,8,9] if x+y==5]
[(0, 5), (1, 4), (2, 3), (3, 2), (4, 1), (5, 0)]

This article is about overloading ; which the above seems to be drifting away from. So what does our overloaded semicolon operator (>> and >>=) look like in the list monad?Lets look at f >>= g. In general, this runs f then runs g feeding in the result of f - onto that behaviour we add our monad-specific behaviour. Lets look at how this behaves in a simple [] monad expression to increment the numbers in a list.First define increment:

increment x = [x+1]

which is used like this:

increment 10
11

Now use increment in a monadic expression:

[1,2,3] >>= increment
[2,3,4]

What did >>= do here?It seems to have run increment three times, to increment three different numbers. And indeed it did. In the [] monad, our sequencing operator will run its right hand side operation multiple times, once for each of the values returned by the left hand side, and then it will collect the results together into a list.How does that tie into the do notation? It means that when I say x<-[4,5,6], then the whole rest of the program will be run three times - once with x=4, once with x=5 and once with x=6, and then the final result of the program will be joined together in a list.Almost done with rambling for now, but I'll make one final comment:I used increment twice in the above text, once with the Maybe monad:

increment x = Just (x+1)

and once with the [] list monad:

increment x = [x+1]

These are almost the same - they both mean "return a value" in the language of the particular monad they live in.But just as >> and do syntax is independent of the particular monad being used, there is an independent way to "return a value", using return:

increment x = return (x+1)

When you use increment in the Maybe monad, then it will mean Just x+1, and when you use it in [] then it will mean [x+1], but even better, someone else can use that definition of increment in a monad that I have never even heard of - because return will do the 'right thing' whatever that happens to be.

ok definitely enough rambling for now.

making haskell EDSLs shebangable

2010-05-07T15:43:00.000+01:00

There's a mindset that says to solve your problem, first write a language to solve your problem in, and then solve your problem in that language. And there's a mindset that says that your language should be an embedded language inside Haskell. In many ways that is appealing.

I wanted to write something that would delete old rsync snapshots. I took the domain-specific language approach, where the language specifies the retention policy for snapshots, like this:

policy = recent <||> weekly <||> monthly

meanings the final policy is to keep 'recent', 'weekly' and 'monthly' backups, with other statements defining what those three other policies mean. I won't write more about the language here - there's more on the webpage for the tool, snaprotate.

One particular piece of this I don't feel terribly comfortable with, and thats how to invoke/run the policy files.

I can imagine two different interfaces:

$ snaprotate -f policyfile

$ policyfile

I took the second approach, making policies first order unix executables - commands that can be run like any other command.

In unix tradition the way you indicate the language of a script is with a shebang line (#!/something) at the start of the script.

So then I want my scripts to look like something like this:

#!/usr/bin/snaprotate

policy = recent <||> weekly <||> monthly

This is almost a valid Haskell program, but: i) I need to import the SnapRotate module, and ii) I don't want to specify a main routine (which looks something like:

main = runPolicy policy

).

So the snaprotate commandline looks almost like runhaskell but does some source file rearranging to address the above two points, and to remove the #! shebang line.

#!/bin/bash
FN=$(mktemp /tmp/snaprotateXXXXX).hs
FNHS=$FN.hs
LIBDIR=$(dirname $0)

cat > $FNHS << 32804384892038493284093
import SnapRotate
main = runLevels policy

32804384892038493284093

cat $1 | grep --invert-match '^#!' >> $FNHS
shift
runhaskell -i$LIBDIR $FNHS $@

I wonder if this is the best way to implement such an embedding?

ALTER

2010-05-01T12:01:00.001+01:00

I discovered the ALTER command in COBOL, in this note on eliminating that command, allowing self-modifying code. A couple of quotes:

ALTER changes the destination of a GO TO statement elsewhere in the program. It complicates the task of eliminating GO TO, especially if you don't notice that the ALTER is present.

and even worse:

In the presence of segmentation, ALTER can behave in unexpected ways. If an independent segment contains an altered GO TO, and the segment is overlaid and then reloaded, the GO TO is reset to its original destination.
If you ever encounter this form of pathology, proceed with extreme caution. You have found either a bizarre and subtle bug or a vicious marauding style of programming. Quite possibly both.

google chart venn diagram of disk usage

2010-04-24T00:01:00.003+01:00

This compares disk usage of a backup I made of /home two years ago with one made this month. There's a lot of overlap - more than I expected.

Method: creating the second backup, I used rsync with --link-dest specified; for measuring, I used du -hsc old new; du -hsc new old. The size of the overlap is the size of new given by the second du minus the size of new given by the first du.

I'm trying to figure out ways of showing overlapping disk usage for more than two or three rsync trees created in this way (for example, to visualise monthly, weekly and daily backups over a long time period)

versions from version control systems

2010-04-17T00:01:00.000+01:00

Sometimes its nice for built software to contain version information from the version control system - this means less to users and more to developers.

This is useful when people, for whatever reason, incorrectly report their version: "please test the release candidate for version 1.0 // I found bug B // That's strange because I thought bug B only got introduced yesterday in the dev code // oh yes, well I checked out the dev code and tested that, not actually version 1.0"; or "I have a new bug C // Are you building from a pristine source checkout? // Yes // Why does your log file contain a warning message that the source was modified? // oh, well I hacked at component Q // yes, that's why you're seeing bug C."

Different version control systems have different version representations. SVN has a sequential revision number; git has directory tree hashes; darcs doesn't seem to have any explicit version representation.

So here is code I've used at different times for svn, git and darcs:

For darcs, here's code I found in darcs issue tracker 1142:

echo "$(darcs show tags | head -1) (+ $(darcs changes --count --from-tag .) patches)"

which gives the most recent tag in the repository and how many additional patches have been added:

v1.1 (+ 39 patches)

For svn, we used something like this in Swift

R=$(svn info | grep '^Revision' | sed "s/Revision: /$1-r/")
M=$(svn status | grep --invert-match '^\?' > /dev/null && echo "($1 modified locally)")
echo $R $M

which we use to form version strings like this:

swift-r1833 (swift modified locally)

Using git-svn, so that I was interested in the SVN version information rather than git version information, swap out R and M above for these:

    R=$(git svn info | grep '^Revision' | sed "s/Revision: /$1-r/")
    if git status -a >/dev/null ; then
      M="($1 modified locally)"
    fi

Both of the above two return the version of the last change in a particular checkout. When there are many modules, its sometimes desirable to give version information for those modules independently. The svnversion command that gives that:

svnversion -c somecomponent

that will produce different output forms that vary depending on the state of the checkout but at simplest gives something like:

To get similar per-directory handling for git, you can do something like this anywhere except in the root of a repository:

SUBDIRPREFIX=$(git rev-parse --show-prefix | sed 's%/$%%')
cd ./$(git rev-parse --show-cdup)
git ls-tree HEAD $SUBDIRPREFIX | (read a b c d ; echo $c)

which will emit a tree hash.

So there are a bunch of different techniques for different version control systems. It would be nice if they were all a bit more consistent - really cool would be a single command that knew all version control systems and could output in a consistent format.

size as a hash function

2010-04-10T00:01:00.001+01:00

Sometimes its been desirable to de-dupe a large collection of data files.

I wrote a tool called lsdupes to do that.

Originally, it was going to run md5sum to hash every file, and then list files with matching hashes to be deleted.

To optimise it a bit, I put in a size check: a first round happens looking at the size of each file, and only when there are multiple files for a given size will md5sums be computed. I though this would the md5sum load a bit.

It turns out that in my photo collection of 44590 photos and videos, the size is a perfect hash - there are no photos with the same size that have different content.

So while md5sum does get run on the dupes, it doesn't find anything different from what the size-based hash does; and the size-based hash runs a lot faster: to walk the tree and get sizes takes around 15 seconds. To then take md5sums of the roughly 5000 files that have non-unique size takes around 7 minutes.

HTML forms in the early 90s

2010-04-03T00:01:00.006+01:00

Before HTML forms used the <form> tag, there was a simpler mechanism called <ISINDEX>. I was reminded about this because someone asked why CGI examples showed urls without name=value pairs in the ?query section, like this: http://ive.got.syphil.is/disease-registry.html?pox

I then went to see if <ISINDEX> still worked in modern browsers. I discovered that in
Safari, it renders a box, but there seems to be no way to submit the query (traditionally, pressing enter would submit it). Lynx and w3m still support it.

From others, I hear:

apparently the default browser on the g1 doesn't even recognize isindex as some sort of input field, although it renders it as such.
sort of weird; won't let you type in it but it renders an input box

and Chrome is also reported to work correctly.

Anyway, this post has an isindex tag right here:

<--- there, so you can see how it works in your browser...

stack trace in perl

2010-03-27T00:01:00.001Z

As a user, I hate java stack traces (because they expose the guts of the program, when I don't care about those guts). But as a programmer, I have come to realise how much I like them, when faced with errors like this:


Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.

where the error is actually deep inside the call on line 27.

So googling around I found this line to put at the start of a program:


$SIG{ __DIE__ } = sub { Carp::confess( @_ ) };

which replaces those short die messages with a stack dump produced by Carp:


Can't call method "emitCode" on an undefined value at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27.
 at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 7
 Stupid::C::__ANON__('Can\'t call method "emitCode" on an undefined value at /Users...') called at /Users/benc/src/stupid/stupid-crypto/src/Stupid/C.pm line 27
 Stupid::LanguageWrapper::emitCode('Stupid::LanguageWrapper=HASH(0x8ff9b4)') called at ../src/stupid.pl line 44

which I hope I'll find more useful...

so many ways to hash

2010-03-20T12:00:00.002Z

I was making commandline tools for stupid to drive the example sha256 code, resulting in multiple tools that deliberately did the same but using different language backends. Then I realised I have a shitload of (where shitload==4) md5sum commandline tools already:

$ echo abc | md5
0bee89b07a248e27c83fc3d5951213c1

$ echo abc | gmd5sum
0bee89b07a248e27c83fc3d5951213c1  -

$ echo abc | openssl dgst 
0bee89b07a248e27c83fc3d5951213c1

$ echo abc | gpg2 --print-md md5
0B EE 89 B0 7A 24 8E 27  C8 3F C3 D5 95 12 13 C1

seq

2010-03-13T14:50:00.000Z

You(*) whisper to X, "the same package [GNU coreutils] which provides seq"
You(*) whisper to X, "the command line utility"
You(*) whisper to X, "also provides factor"
You(*) whisper to X, "which outputs prime factors"
You(*) whisper to X, "makes me want to start making fucked up shell scripts"
You(*) whisper to X, "that use goedel numbering"
You(*) whisper to X, "for some purpose."
You(*) whisper to X, "i have to wonder how a commandline utility for factoring primes is 'core' in any way, though"

ASCII art C++ constants

2010-03-06T01:00:00.000Z

I came across Multi-Dimensional Analog Literals in C++. This is an implementation in standard C++ templates that lets you write constants out using ASCII art (in 1, 2 or 3 dimensions):


  unsigned int c = ( o-----o
                     |     !
                     !     !
                     !     !
                     o-----o ).area;

  assert( c == (I-----I) * (I-------I) );

I think the same would be straightforward to implement using Template Haskell's quasiquoting mechanism, which allows you to embed parsers for fairly arbitrary sublanguages inside Haskell source. I wonder what other languages you could also implement something like this in.

slide controller

2010-02-27T21:13:00.002Z

I just brought my third one of these:

(my first got lost at an event a few years ago, and I lost the USB dongle for my 2nd a few months ago)

If you want something to change your PowerPoint (or powerpoint-like) slides, this is the tool to get. Its worked with every computer I've tried it on, and every piece of presentation software (PDF viewers and HTML slidy in addition to PowerPoint and Open Office).

No software to install either - the dongle appears as a USB keyboard - the four keys send PgUp and PgDown to change slides; the laser beam button sends an F5 (which is start-presentation in PowerPoint) and the bottom button sends 'b' (which is blank screen in PowerPoint).

binary numeric promotion in java numeric types

2010-02-27T10:59:00.007Z

I've been working on a Java backend for stupid, a crypto algorithm language proposed by Ben Laurie.

This has led me to look at Java numeric types a little more closely (and with a decade more cynicism than last time).

I'd forgotten entirely that there were short and long numeric types - for pretty much any use I've made of numbers in Java ever, int has been fine.

short behaves a little surprisingly:

If a and b are both long, then a & b is a long.

If a and b are both int, then a & b is an int.

If a and b are both short, then a & b is an ... int. wtf. why?

Likewise byte & byte -> int.

This is specified in 5.6.2 Binary Numeric Promotion of the Java language specification.

(later:)
Its pointed out that C also does implicit casting of smaller types to int; but gcc is a little gentler with its warnings. a+b gives a warning (not an error) similar to the Java code above, but a&b does not (presumably because it knows that this can't make the number be any bigger than the types you started out with... something that gets lost in the Java type checking)