Tellur52の日記: Coqすげー
日記 by
Tellur52
表の記事のコメント経由でCCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介を読んでたまげた。
SSLのハンドシェークをCoqで実装できるか考えると、特定のメッセージを送受信できる条件が明確になって脆弱性が分かるんだ!
(誰もCoqでセキュアなコードが楽に書けるとはいってない)
.
Coqって、解説読んだだけでちょっと挫折したけど、
Prologみたいに!でごまかしたりせずに論理の証明をするシステム、
みたいなのか・・・な・・にゅ・・それにしても大鯨かわいいな、
と、意識はあらぬ方向に逸れていく。。。
Coqすげー More ログイン