3 ms·
I'm curious if folks tried to use a model checker. Seems like a model checker might be able to identify cases in the spec where invariants are violated.
by sunshowers 2y ago
I'm curious if folks tried to use a model checker. Seems like a model checker might be able to identify cases in the spec where invariants are violated.
- lxgr 2y agoI don't think that that would have helped here: The invariant ("URLs purportedly resulting from a QR code scan must only result from an actual QR code scan") essentially follows directly from a specific threat scenario that was missed.
- sunshowers 2y agoYeah, you're right, that does seem to be very specific.