💾 Archived View for republic.circumlunar.space › users › dbane › gemlog › 2022-03-22.gmi captured on 2024-08-18 at 18:14:43. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

An Increased Security Posture

Previous blog posts assumed a threat model of criminal organisations running ransomware. So I was interested in safe languages like Lisp and D (with the @safe annotation). There is some kind of migration path from existing systems to here. Similarly, although I didn't mention it running on OpenBSD is another low-cost way to improve security.

Very recently the international situation changed, such that now it's not inconceivable that your threat model is a nation state. This changes the cost/benefit calculation.

I think static typing, with an adequate (e.g. Hindley-Milner, inference, sums & products) type system, is required. So all the subsequent points assume the programming language is Standard ML.
Can adopt two design patterns to increase reliability/security: design-by-contract from mltonlib and Kiselyov's "lightweight static capabilities"
I still want to avoid two languages for prototyping & production, so "design through documentation" should be used. Recall the documentation can be delivered at the same time (not necessarily beforehand)
Not really security-related, but mltonlib also includes build functionality, so sml-buildscripts aren't needed any more

MLton Library Project

Lightweight Static Guarantees

The main disadvantage of this rigour is tht you lose some of the flexibility to do iterative prototyping in code. Instead, you could continue my old research and "design through documentation", it will work albeit maybe not as quickly. This works best with copying & hardening features of existing systems instead of dreaming up new product categories, e.g. "copy an existing MUD server/IRC bot".

In terms of the TCB, both options are pretty much the same. There is more C code in an ML runtime than EISL, but on the other hand it probably has more users. And it means we don't have to maintain it (or is it that we can't maintain it?) We lose a potential product, a hardened Lisp interpreter, but I'm not convinced the world needs yet another Lisp interpreter either.

So the question is, does the somewhat higher quality of the final code justify the more clumsy prototyping phase using documents? And this depends on your threat model, but my current thinking is that as of a few weeks ago, for server code where you have most of a design to copy it is worthwhile. For other scenarios, no.

Unit testing isn't enough. You need static typing too.

One thing that has become clearer to me is that when I mentioned moving tasks "back" in the V model, e.g. testing to contracts in code, this was incorrect. Instead, I want to move them *down*, e.g. as well as the above, move formal spec documents to contracts (and types) in code. This is another reason to use a sufficient type system.

Finally, I prefer to restrict this blog to technical content, but I *do* personally feel the war to be a clear violation of international law, from the Treaty of Westphalia onwards.

Background: Why Standard ML

It's not the most important decision so feel free to skip this, but here are a few things that I like about SML. There are other languages that satisfy these requirements, e.g. Rust is popular now but I think SML would be easier to write.

I already know it. This is probably the most important one.
It has a vendor-neutral standard.
It has several implementations.
At least some of the implementations support multiple cores.
At least some of the implementations compile to native code.
The language is more amenable to reasoning/proving than usual.

The prototyping story isn't as good as a dynamically-typed, homoiconic language; but that's a price that's worth paying in some security environments.

Back to my gemlog