In the time that it takes a sophisticated attacker to find a hole in Azure that will cause an hour of disruption across 1% of VMs, that same attacker could probably completely take down ten unicorns for a much longer period of time. And yet, these attackers are hyper focused on the most hardened targets. Why is that?
I suspect it’s the same reason that people will flock to play the 1 Billion dollar PowerBall, but the still life changing $30 Million lottery jackpot isn’t as enticing.
Humans are terrible at risk/reward judgement. They also won’t pay the same amount for a 1/20 raffle ticket. Some of them still smoke, don’t wear seatbelts and keep guns in the same house as their own children.
some of them even keep dangerous drugs like Acetaminophen in the same house as their own children.
sigh Yes, I don’t own any acetaminophen. I’d rather have exactly one available suicide method, so that I can never think about it or come upon it accidentally, but be reassured that it’s there so that I never need to have panicked thoughts about not having one. I think a lot of people with mental health stuff take that particular caution pretty seriously. :)
Honestly, I’m not sure whether you were trying to be sarcastic, but it IS a dangerous substance, if you specifically intend to use it that way, and the information about how to use it is readily available. If I were caring for children I’d be pretty cautious about having it around.
(Note: The most recent attempt was quite a few years ago and I’ve had a lot of life changes since then and have no intention to die in the foreseeable future. Just in case there’s anyone reading this who doesn’t understand how this stuff never goes away, and is afraid on my behalf. There’s no need for such fear.)
I would say that using a less mind-bogglingly complex ISA would reduce the likelihood of these issues. But having fixed so many stupid bugs in RocketChip over the last year, I’m not so convinced. There’s no way to make things completely bug-free. There’s just way too many weird corner cases.
Verification of FM9801 (2002) says the proof of the microprocessor design was checked by a theorem prover, so it’s apparently possible. Has there been more progress on this front?
I think one issue is how do you verify a multicore processor? Sure, for a single core cpu, you can generate a formal spec from the ISA manual. But how do you specify the myriad interactions of a multicore system.
https://media.ccc.de/v/32c3-7171-when_hardware_must_just_work is directly relevant to this question. Formal proof is only a part of cpu design.