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.
replyI 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.
replyFor 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...
replyYour version is likely good enough in practice though.