3 ms·
My takeaway is that using formal methods is difficult to turn into any sort of actual security guarantee, due to the difficulty of connecting them to a real wor
by albntomat0 7y ago
My takeaway is that using formal methods is difficult to turn into any sort of actual security guarantee, due to the difficulty of connecting them to a real world system in a meaningful way. While formal methods could produce something meaningful with proper "inputs", getting that done is hard.
- MaxBarraclough 7y agoI'm more optimistic. There's real value in building ultra-low-defect crypto code, and as far as I can tell, formal methods have a good track-record there. We already knew that integration into non-verified code isn't guaranteed to be free of defects - that's out of scope by definition. That's somewhere safe languages can help though. What the paper describes as corrupted data might well be the kind of bug that often happens in C, but rarely happens in a safe language. The other question is vulnerability to side-channel attacks. Today's formal methods aren't much use against them.