verberant

In a past life, I pushed hard for more investment in seL4 for certain defense applications. The nuance isn't to be underestimated though – I can say from experience that it's often a hard sell to folks that aren't already versed in the ins and outs of formal methods, security, kernels/operating systems, etc. There are plenty of lower hanging fruit (like networking hardware) than the applications I worked on, yet commercial adoption still seems low. Maybe this is due to that nuance. To the credit of the folks at Trustworthy Systems and UNSW, they've done a great job producing literature that outlines the business case in a manner palatable to decision makers. This paper [0] in particular came in handy to me many times.

[0] https://ts.data61.csiro.au/publications/csiro_full_text/Klei...

> And this leads me to the conclusion that software quality is mostly driven by the company and economics. If the project doesn't pay for solid quality assurance or has too much time pressure on developers, the software you get might be bad at least to some degree. Even good developers can't make up for that.

I think this is absolutely the case. As an extreme example, an organization that uses formal methods is probably going to ship higher quality software because they've meticulously worked out design bugs before they've even written a line of code and, once the program is implemented, they've rigorously verified its correctness – the economics of this methodology, however, are not really feasible in most circumstances and so instead we opt for duct tape fixes and crunch time.

The author also mentions the lack of gatekeeping for software engineering – this is often pointed to as one reason for bad software existing. I tend to agree, since "good code" and "bad code" that both do what they're supposed to under the common case can appear the same to the user and the manager who signs off on it (excluding bad UI). Point being, if someone can code just well enough to get by in their field, they will probably remain employed. This is a tricky problem to solve though, because so much of the practice of software engineering is qualitative (bordering on aesthetic, I would argue) and involves designing abstractions. While much of software engineering is analytical and must obey a certain set of axioms, higher-level systems and software design is really more akin to art and architecture than civil or mechanical engineering.

Space flight computers in the public sector are generally 15-20 years behind the types of hardware we commonly work with on the ground, as I think this page shows.

We now have pretty capable low-power SoCs and FPGAs that we've yet to see broadly leveraged for govt. space applications. SpaceX flies Starlink with Xilinx FPGAs, while NASA and DoD are still baselining new platforms on incredibly expensive (albeit rad-hard) PowerPC RAD750 and similar. This is a huge bottleneck for any computationally intensive task we might want to do on-orbit, and I'm curious if or when it will change. It's one technical reason, in my opinion, that the private sector is currently calling the shots in space.

While serious, this should come as no surprise to anyone who has had the "pleasure" of using a government IT system. The OPM hack a few years ago demonstrated this and the current SolarWinds crisis just reminds us of it.

You could liken the security issue to climate change – our entire global economy appears to depend on consumption, which appears to be accelerating climate change. But are we going to actually change anything significantly to address the problem? Uh no, not now, maybe later. Most people barely understand the problem and, even if they care, are powerless to change it. Furthermore, we are now completely reliant on the status-quo and seemingly incapable of imagining a different world. In the same manner, these software systems which now underlie every part of our day-to-day lives are taken as a given. They are now simply too convenient and ingrained in our lives to ever go away.

How do we overcome the inertia of change? Most likely, from what I can see, we will simply change our expectations – it is impossible to build a completely secure software system, so we should instead change how we use it/what we expect it to do.

We also feel pressure to constantly modernize the infrastructure without having a parallel discussion about the security impact of these innovations. As we get further and further from the bare metal with newer and more convenient abstractions, our engineers understand less and less about the realities of the systems they are constructing. And, arguably, as software becomes easier for users to use, they too lose sight of what the system is actually doing and how something can go wrong.