No mention of Spectre or Meltdown? I'm all for improving formal verification but their method ignores the fact that there are leaky abstractions throughout the

No mention of Spectre or Meltdown? I'm all for improving formal verification but their method ignores the fact that there are leaky abstractions throughout the stack, those of which enable vulnerabilities. That is, this seems like total BS: > we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification Edit: they do mention it: > Side-channel attacks [20],[21], [22], [23], [24], [25] are beyond the scope of the paper So basically they've developed a method for formally verifying components of systems, by making assumptions about the periphery.