Lambda the Ultimate

The recent discussion around Safe and Secure Software in Ada involved some amount of discussion around what is involved in proving software secure, and what role do PLs play in this. I'd like to recommend two papers to advance this discussion:

• First, Rao & Rohatgi (2001)'s EMpowering Side-channel attacks, which discusses a fairly new technology for gathering information from running systems by monitoring their EM emissions; and
• Rae & Wildman (2003)'s A Taxonomy of Attacks on Secure Devices, which provides a synthetic classification of attacks on computer systems based on the attackers degree of access to the machinery and the attacker's objectives, and which catalogues a range of attacks into the classification.

So I hereby advance three slogans:

1. Security is physical: neither applications nor operating systems can satisfy elementary security properties, but only deployed computer systems. This is because elementary security properties are about what the attacker does, which ultimately has a physical basis;
2. Security is non-modular: Programming languages and software engineering practices can ensure that software possesses properties helpful to security, but the properties are only meaningful in the context of a strategy to ensure a computer system satisfies its security policy;
3. We should not talk of secure programming languages and secure programs, such talk does mislead; to talk instead of software being secureable might promote better understanding.

Edited following Dave Griffith's remarks.

Just came across the Fan object-oriented programming Language, running on the JVM and the CLR. They're shooting for portability across both VMs. Looks like they took an interesting approach language-wise, such as default immutability for concurrency, closures, mixins and exporting namespaces as REST-like URIs. This last feature is one I first encountered in the Waterken capability-secure HTTP application server.

I was disappointed to read that Fan eschews generics/parametric polymorphism however. All told, it seems to lean slightly more towards the dynamic end of the spectrum than C#/Java.