AWS × 形式手法で人知を超えたセキュリティを手に入れろ
システムを数学的対象として記述すること(形式手法)で
直感に頼ることがなくなる。ただし習熟者は少なく学習コスト高め。
理解できなかったため、少し調べてみた。
形式手法
「テストでは、欠陥が無いことは保証できない」(Edsger W. Dijkstra)
この問題を解決するため、形式手法では、仕様を数学的に記述し、テスト漏れがないことを証明する。
形式手法とモデリング – AlloyAnalyzerを中心に
モデル検査機 Alloy
java -jar "C:\Users\shimizu\Downloads\alloy4.2_2015-02-22.jar"
とすることでAlloy Analyzerが起動した。
試しに1つ実行してみた。
sig User { policy : Policy, } sig Policy {} run {}