3 ms·

"Continuous formal verification of Amazon s2n" (2018) https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 https://link.springer.com/chapter/10.1007/9

"Continuous formal verification of Amazon s2n" (2018) https://link.springer.com/chapter/10.1007/978-3-319-96142-2_26 https://link.springer.com/chapter/10.1007/978-3-319-96142-2_... https://scholar.google.com/scholar?cites=2686812922904040715&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=2686812922904040715... But formal methods (and TLA+ for distributed computation) don't eliminate side channels.

quotemstr 3y ago
> But formal methods (and TLA+ for distributed computation) don't eliminate side channels. True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.
- rewmie 3y ago
  > I'm normally aghast at people writing new code in plain C, Why?
PhilipRoman 3y ago
There have been some attempts at formally verifying lack of timing attacks (to the extent allowed by hardware). This is the one I know the most about: https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 but there are likely others
- folmar 3y ago
  Also in around side channel topic for example: E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, EUROCRYPT 2013, LNCS 7881 S. Dziembowski and K. Pietrzak, "Leakage-Resilient Cryptography, 10.1109/FOCS.2008.56.
  - westurner 3y ago
    Side-channel: https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack Time complexity > Constant time: https://en.wikipedia.org/wiki/Time_complexity#Constant_time https://en.wikipedia.org/wiki/Time_complexity#Constant_time "Masking against side-channel attacks: A formal security proof" (2013) https://link.springer.com/chapter/10.1007/978-3-642-38348-9_9 https://link.springer.com/chapter/10.1007/978-3-642-38348-9_... https://scholar.google.com/scholar?cites=14793554920974372767&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=1479355492097437276... "Leakage-Resilient Cryptography" (2008) https://ieeexplore.ieee.org/abstract/document/4690963 https://ieeexplore.ieee.org/abstract/document/4690963 https://scholar.google.com/scholar?cites=5581902451405085906&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=5581902451405085906...
- westurner 3y ago
  "FaCT: A DSL for Timing-Sensitive Computation" https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 citations in gscholar: https://scholar.google.com/scholar?cites=15701999263081018564&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=1570199926308101856...

quotemstr 3y ago

> But formal methods (and TLA+ for distributed computation) don't eliminate side channels. True, but they eliminate whole classes of attack. I'm normally aghast at people writing new code in plain C, but formally verified plain C counts as a whole other and better paradigm to me.

rewmie 3y ago
> I'm normally aghast at people writing new code in plain C, Why?

PhilipRoman 3y ago

There have been some attempts at formally verifying lack of timing attacks (to the extent allowed by hardware). This is the one I know the most about: https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 but there are likely others

folmar 3y ago
Also in around side channel topic for example: E. Prouff and M. Rivain, Masking against Side-Channel Attacks: A Formal Security Proof, EUROCRYPT 2013, LNCS 7881 S. Dziembowski and K. Pietrzak, "Leakage-Resilient Cryptography, 10.1109/FOCS.2008.56.
- westurner 3y ago
  Side-channel: https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack Time complexity > Constant time: https://en.wikipedia.org/wiki/Time_complexity#Constant_time https://en.wikipedia.org/wiki/Time_complexity#Constant_time "Masking against side-channel attacks: A formal security proof" (2013) https://link.springer.com/chapter/10.1007/978-3-642-38348-9_9 https://link.springer.com/chapter/10.1007/978-3-642-38348-9_... https://scholar.google.com/scholar?cites=14793554920974372767&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=1479355492097437276... "Leakage-Resilient Cryptography" (2008) https://ieeexplore.ieee.org/abstract/document/4690963 https://ieeexplore.ieee.org/abstract/document/4690963 https://scholar.google.com/scholar?cites=5581902451405085906&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=5581902451405085906...
westurner 3y ago
"FaCT: A DSL for Timing-Sensitive Computation" https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 https://dl.acm.org/doi/pdf/10.1145/3314221.3314605 citations in gscholar: https://scholar.google.com/scholar?cites=15701999263081018564&as_sdt=5,43&sciodt=0,43&hl=en https://scholar.google.com/scholar?cites=1570199926308101856...