syntactically correct type-checkable /* NOTIMPL */

Agda, a dependently typed programming langauge Agda has a neat feature for partially written code.

Often I'll flesh out code and write something like a TODO inline. I'm sure lots of other people do to.

(For example, in C:

  int x;
  x = TODO_CALCULATEX();

This won't compile, so you don't get the benefit of compile time checking on your code until you've fixed up all your TODOs into something that makes sense to the compiler: either implementing it, or implementing a stub (an extreme case of which might be to replace the whole function call above by the constant 0).

In C and other languages which don't do much in the way of correctness checking at compiler time, thats ok.

For a lot of uses of Agda, the compile time checking is where all the interesting stuff is, though: for example, Agda types are where you put proofs like "this sort function really does sort".

Its a bit more awkward to make up stubs that claim in their comment or name to do something, whilst not doing it, because there is usually a lot more stuff in the type signature (such as the assertion that this sort function really does sort). You can't just put a return 0; and have it type check ok.

So, Agda uses a special extra bit of syntax: _ (an underscore) to mean "I have no value for this; but please pretend to all intents and purposes that you do." That way, compile time checking can carry on. Agda understand that its a TODO that you'll get to later on. Or even in some circumstances figure out the value for you.

2y

this blog is 2y old today! I'm writing this way back in May 2011, though, so there's a pretty high chance that it could have been dead for a few months by the time you read this though ;)

bugs that never go away

I had a problem trying to get mrtg to read ssCpuRawUser.0 and related snmp variables. it was giving some error, even though it can read various other snmp variables fine. i googled. I got a few pages of people going all the way back to 2001 with the same error. no solutions. there's even a bug where the mrtg author WORKSFORMEs it. fuck this. I think there's an XKCD about this. So, I can read the variable with the net-snmp commandline tool and feed it in that way. yay for being able to write my own plugins.

#!/bin/bash
# $1 = name1
# $2 = name
# $2 = host
snmpget -m + -c public -v 1 $3 $1 | sed 's/^.*Counter32: //'
snmpget -m + -c public -v 1 $3 $2 | sed 's/^.*Counter32: //'

dmarc

A bunch of email providers announced DMARC which builds on top of SPF and DKIM to allow domains to specify more policy when SPF and/or DKIM fail.

I already have SPF and DKIM set up on my personal domain, hawaga.org.uk, which has been round for over a decade. I run mail servers for various other domains, but those are much younger and much less widely used.

Its been hard to quantify how much this has helped/not helped. I don't get complaints about spam originating from my address. I used to get a lost of postmaster backscatter but not any more - not sure why, though I can invent various possible reasons.

One of the interesting things with DMARC is that it claims to provide feedback about what filtering is happening, from receiving/filtering parties - that makes it especially interesting, I think.

So, given that I already have DKIM and SPF, what extra do I need to do to get something useful from DMARC?

I need to publish a policy in DNS, under my sending domain. (this is also how SPF and DKIM do things)

So I've put in this policy on the 4th of Feb:
_dmarc.hawaga.org.uk. 3583 IN TXT "v=DMARC1\;p=none\;rua=mailto:benc@hawaga.org.uk\;ruf=mailto:benc@hawaga.org.uk\;ri=3600"
That says to not enforce any policy, but to email benc@hawaga.org.uk with reports every 3600 seconds (= 1 hour).

I set this up at about 5pm on a Saturday and about 11am on Sunday morning my first report arrived, with a timestamp range of a day, which must extend back before I turned this on...

In there, three messages from my main outbound mail server, and no others.

Lets see what else I get...

A couple of weeks later...

I got daily reports most days from Google (I think maybe the day I didn't get a report was because I hadn't sent any mail into google all(?)).

A few days after the above I added in two other domains: my company domain with only occasionally sends mail, and my girlfriend's vanity domain. Neither of those have SPF or DKIM on them, even though they come from the same mail servers as hawaga.org.uk.

There was a noticeable lack of reports from anyone other than Google. I asked around (on Google+) to see if anyone had reports from elsewhere (eg AOL or Yahoo, because those were also listed) but no one said yes.

So what about the reports?

Well, there were surprisingly more mail servers than I expected: along with my own two outbound servers, there were about 10 other servers, being the outbound mail servers of a handful of research institutes that I work with. Those reports were tagged by google as being via a mailing list. Its not clear to me what defines a message as being via a mailing list, but I guess it would mean that they'll put less weight on my SPF records? It also highlights how a naive interaction between mailing lists and SPF can result in your message being treated as spam.

I also got some DKIM fails reported from my own legitimate mail server. The best I have been able to diagnose there is that I had sendmail set to deliver mail without a DKIM signature if the dkim milter timed out; but if that's going to contribute negatively to spam treatment, then I think a better configuration is to have the milter set to retry later, resulting in more delayed mail, but more DKIM-signed mail.

The extra domains I added had no DKIM on them, but those weren't treated as DKIM-fails. Instead they were reported as DKIM 'none'. I'm not sure what causes none rather than fail, but my guess is its something to do with the fact that hawaga.org.uk has DKIM records in its DNS, and thats being treated as an indication that there should be DKIM signatures on messages. I think that's extra meaning that I hadn't understood DKIM DNS records to mean.

I have a similar confusion with the interaction between SPF and DMARC: SPF has multiple output states, not just pass or fail, and its not clear to me how those are treated by DMARC.

Processingwise: the reports come as zipped XML documents. It was relatively straightforward to munge these like any other XML (though I made it harder for myself by learning a new Haskell XML library rather than using ones I already knew).

Its unclear to me how I know that a report really is from a particular sender, and what the threat model is for people injecting false DKIM reports - perhaps injecting them to suggest that people's use of DKIM and SPF is causing their mail to be dropped, and thus encouraging them to turn off SPF and DKIM?

So for now, I'll keep this switched on, in monitoring-only mode. I don't feel I understand it well enough to turn it on in enforcement mode (especially as I'm not the only user sending mail under hawaga.org.uk. I think its very interesting and probably useful to be able to specify policy this way; but the policy language at the moment feels either vaguely defined, or at the least not concisely described, in a way that makes me comfortable.

DKIM - domainkeys identified mail

Looks like I never wrote a blog posting on setting up DKIM. I just realised one of my servers wasn't set up after a re-install, so I'm having to remember how to do it again.

I'm using sendmail. (yes, shut up) and DKIM hooks in using its milter (mail filter) mechanism.

# apt-get install dkim-filter

Now wire it into sendmail.mc:
INPUT_MAIL_FILTER(`dkim', `S=/var/run/dkim-filter/dkim-filter.sock')

Now when mail comes in, you should see it gets headers like this added by your mail server (dildano.hawaga.org.uk in this case) when DKIM verification happens (eg in mail from gmail).:

Authentication-Results: dildano.hawaga.org.uk; dkim=pass (1024-bit key)
 header.i=@hawaga.org.uk; dkim-adsp=none

The other half of the equation is DKIM signing my outbound mail, so that other people who do checks like this can verify/not-verify my email.

DKIM needs a public/private keypaid

# dkim-genkey -b 1024 -d hawaga.org.uk -s hampshire

-s specifies a selector name. This is a fairly arbitrary identifier used to identify this keypair, because a domain can have multiple keypairs (for example, one per mail server). In the hawaga.org.uk domain, I seem to use names of English counties.

# ls
hampshire.private  hampshire.txt
# cat hampshire.txt
hampshire._domainkey IN TXT "v=DKIM1; g=*; k=rsa; p=MIGfMA0GCSqGSIb3DQEBAQUAA4GNADCBiQKBgQDUP+5f0nEWyYICxr8rLN8xannlteBg4WF2Fat/MS8CiAa1lE2wgvhKYJJD/ydJ//5B9fBZAwSXTAq2ZCQYIfRf985Yip0BK80ECTlOunaSnMY/4/RzmkXGpndJaHIFqmSWDhML1yBP6W6owJDXIPDCAbV80kd5Z5aAkv8518lk+wIDAQAB" ; ----- DKIM hampshire for hawaga.org.uk

That .txt file is a DNS record to install under hawaga.org.uk. When you've installed it, you can check with:
dig -t txt hampshire._domainkey.hawaga.org.uk @localhost

That's the public key installed. Now the private key.

In /etc/dkim-filter.conf:

Domain hawaga.org.uk
KeyFile /etc/mail/hampshire.private
Selector hampshire

# /etc/init.d/dkim-filter restart

Now send out some mail to some other account. It should have a DKIM signature header added like this:

DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=hawaga.org.uk;
 s=hampshire; t=1328349841;
 bh=hGo8Oadbgx3cVNwLr3hGDRfMX5LwWwXuz2PzqEowx0I=;
 h=Date:From:To:Subject:Message-ID:MIME-Version:Content-Type;
 b=oBeSDSzxz7/awSnxuos6jyJuBoYH2MbiB3HDpbZfLQnTTdEJdx2WD0ubSVAaKAJmV
  ma5xuSaNGeS7X3Xg49obL6nWA89tiOeVAq9FO+7NP+v2DmUPFxEYkLeQJUANYKzAw/
  r8ag9XnbRkxvY+J/rrmeaAjJdnfgUQlKSHlV5CWE=

... and if that other account happens to do DKIM verification, you should see its version of:

Authentication-Results: paella.hawaga.org.uk; dkim=pass (1024-bit key) header.i=@hawaga.org.uk

yubikey for encryption, not verification, passwords

I previously mentioned that my yubikey has a mode where it can enter a 64 character fixed string. I've been regarding that as useful in systems that are too closed to support HOTP. But I just realised that they also have a more "sensible" use on systems that due to more fundamental technical reasons cannot have a changing password - where that password is used to actually encrypt data, rather than being verified against an expected password - for example, GPG or encrypted home directories.