Slashdot Mirror

It's amazing how many people still wrongly believe that formal verification guarantees that software is bug-free. The proven properties only hold under certain conditions. In a recent study, researchers from the University of Washington analyzed several verified distributed systems and found a total of 16 bugs in them, some of which could cause the systems to crash or corrupt data. The bottom line is that formally verified software does NOT mean bug-free software and you STILL need to test software. Here's a summary of their findings.

With coins going for so much money, a DDoS would be relatively cheap, in return for the gains involved.

According to Apostolaki et al., the BitCoin network routinely suffers routing attacks already. And by "routinely" they mean at least 100000 times a month.

It would appear that partitioning the BitCoin network is already a widely-used tactic, and that's just BGP attacks - we're not even talking DDoS yet. I haven't looked closely at Lightning (I'm not very interested in BitCoin, personally), but I wouldn't be surprised if (as GP suggested) it will make things worse.

If you like this story, I recommend signing up for the daily computer science paper. I'm not affiliated, just like it. Lots of good stuff there.

tbh this seems like a fertile area for research. Probably many PhDs available in for people who want to work on making formally verifiable permission systems. Just starting to think about the problem here,

You'd need to start with a very simple permission system. For example, Android has so many complex, overlapping, and confusing permissions that holes are easy to find without any thought at all. Basic Unix has a very simple permission system so you could probably work with that, Windows is probably too complex to do reasonable proofs, and modern Linux gets rather complex with all the containers, too.

The next step would be to start looking at individual system calls. Is there a way to formally verify that they aren't going to cause problems outside the rules of the permission framework? Of course there is, and with some of the system calls it's really easy. Other system calls would be very much harder (I'm thinking of select() here).

Once they system calls have been divided into 'easy' 'hard' and 'intractable' (or other appropriate categories), you can get started formally verifying the easy ones, and ideally built an automated system to prove their correctness. Then, in the hard category, there are likely some syscalls that can be moved into the 'easy' category with some simple changes, like unifying code paths that are mostly the same, for example.

You can start chipping away at the intractable syscalls, and eventually move some of them into the hard category, but at least you'll clearly know which syscalls are the intractable ones. Once you know that, you can offer a 'safe' mode in the kernel, where certain processes are not allowed to call those syscalls that are known to be dangerous.

We should be able to reach DJB's goal of, "We will have invulnerable software systems, with no bugs in trusted code. We will be confident that these systems enforce the user's security requirements."

A surprising amount of the resistance is plain fear: if you describe a solved problem in computer science, some number of the PHBs and some of the engineers will be frightened, and push back. Others will cover their ears and say "naa, naa, naa, can't hear that". After all, if they knew it was a solved problems and did the wrong thing, they could get in trouble!

The frightened folks need to keep an eye on the news: I reccomend the morning paper.

The person proposing a known fix should do so either very early in the project's life when it's easy to change, or very late, after a fiasco when it has to change. The middle is A Bad Time to change horses.