The discussion on the cost of the attack needs an addendum. The lattice sieving part would be free for an an attacker with a big enough botnet or enough cloud computing stolen credentials.
Maybe it could even be practical to run it on browser in parallel to video streaming on a free video site...
LLM chatbots may not have a sense of self preservation or a meaningful concept of legal consequences, but they have an excellent model of user engagement. Getting a user to think they are invincible is very good for engagement.
Efficiency is not that that important in an era of negative price electricity.
Synfuel made just from air and electricity is doable (both water and carbon dioxyde can be extracted from the atmosphere). And with 10% of what's spend on IA we'd be way out of the lab...
Thankfully there are military budgets (synfuel makes sense on a nuclear carrier)
Security-partition switches that carefully reset all shared micro-architectural state, while making switch times completely deterministic, and in particular, independent of previous execution history.
I'm afraid it means clearing all caches at each context switch. The performance penalty is really high.
Not all caches are cleared. There are some clever techniques to partition off-core caches (i.e. the L3) as part of the isolation boundaries enforced by the kernel. What I think is particularly exciting is that a new RISCV64 instruction to clear microarchitectural state is in the process of being standardised! So I'm hopeful that, while it should not be ignored, the performance penalty will not be too high.
This has its own issues. Big bad actors can now split their activities between more smaller companies to avoid some regulation. I've seen it happening.
Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels.
So the proof won't be invalidated at it does not cover that particular threat.
Now the question is how useful the is a proof not covering side channels? I'd say pretty useful and it doesn't mean they don't have counter measures for to counter their exploitation, nor that they are not effective, just that a proof of efficiency is out of reach for now.
To add to that, the only way I see proof of absence of timing channels is by proving both the software and the hardware design side by side, and then the proof would hold only for a specific core. Something that would look both at the code manipulating secrets and at the Verilog for the specific core/memory chips. I've not been working in that space in a long while but AFAIK such a thing is nowhere near ready. I suspect it will be a lot easier if the hardware design is optimised for provability, which won't be good at all for performance. But there are plenty of contexts where security matters a lot more than performance (SMC, BMC, RoT and co at the very least).
And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
I don't think you can ignore memory access. The whole "hyperthreading considered harmful" was because of shared cache between contexts. That's why I think a proof is in reach without cache, much harder with one...
Without cache, without virtual memory, without throttling when the more hardware is switched on or the CPU gets hot, without memory that’s unreliable under load (https://en.wikipedia.org/wiki/Row_hammer), etc.
What you want is a proof that microarchitectural timing differences (ie. the difference between a cache hit and cache miss) cannot possibly turn into architecturally-visible timing differences. If a program cannot reliably distinguish between two points in time, time is not a suitable channel for programs.
You could have an ISA where timing information is simply not presented to the programmer, but programmers like being able to profile their programs.
You don't need to prove the hardware correct to prove that the software is free from timing side-channels. You just need a model of the hardware that captures timing information.
Sure a hardware or model bug would render your proof non-applicable, but that is already the case for the existing proofs.
The bigger problem is simply that hardware designers do not care about timing side channels. Even if you did accurately model the timing behavior of a modern processor, you would just discover that trying to write software free from timing side channels is a practical impossibility.
> And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
You would also need to prove that our model of physics accurately describes how that silicon would behave, and the the environment around the silicon is within the physical parameters you modeled...
Interesting, but not unheard of. Think of attacks like Row Hammer. No revolutionary physics needed. But chip designers cannot fully apply quantum field theory to an entire CPU, so they necessarily use simplified a simplified physics model. The resulting chips then need to be empirically verified to correct places where that simplified model diverges to much from the messy reality, which means that the chip design is only as good as the empirical testing done to it.
Add to that the potential for unknown and mis-moddeled manufacturing defects, and manipulated electrical voltages and signals, random particle interactions, and there is a lot of room for known physics to break a verilog level proof of correctness.
I don't think it needs to be so dramatic. You could have a proof that the algorithms don't contain data-dependent logic, and perhaps ensure that no data-dependent instructions are generated; and that all branches have the same number of instrution-cycles (adding padding if not). You'd then simply rely on the architecture-specific instruction timing differences to be respected by the compiler.
Would something like this guarantee that no side-channels are possible on any architecture? Perhaps not, but it would still get you most of the way there.
What about power draw? Maybe that doesn't count as a side channel (I'm not a security guy). Afaik, CMOS transistors mostly draw power on switching state, so a normal adder adding 0+0 or 1+1 is visible in the power draw.
I googled a bit and found Sense Amplifier-Based Logic (SABL). Super interesting :^)
Power draw is a side channel, yeah. It's not as easy to exploit in software as timing (including memory timing), but there are software exploits in some cases if it affects the CPU's frequency (HertzBleed) or if it can be read through channels like a sound card or radio receivers. For attackers who have physical access it's very much in scope.
For software like seL4 it would generally be out-of-scope, because it depends too much on the specific hardware and specific application, not just on the kernel, and protection usually requires extensive countermeasures in those places.
I'm not so sure. It's pretty hard to know how many cycles a register load instruction will take if there is a cache, or worse a cache hierarchy. That's why I think it will be a lot easier to have a proof on simple cache less designs...
Your version is likely good enough in practice though.
It’s absolutely still very useful. Security is risk mitigation, and a reduced surface area makes it easier for everyone to focus on the remaining areas.
It’s basically a great front door lock: it does not guarantee nobody will break in through window, but it narrows the population of threat actors who have time and inclination.
He also has dedicated entries on two very special case, the engine running within pdflatex https://blog.mathieuacher.com/TeXCCChessEngine/ and the one in Brainfuck https://blog.mathieuacher.com/BFChessChessEngineBrainfuck/ which are seemingly the first of their kind.
reply