AWS × 形式手法で人知を超えたセキュリティを手に入れろ

システムを数学的対象として記述すること(形式手法)で
直感に頼ることがなくなる。ただし習熟者は少なく学習コスト高め。

理解できなかったため、少し調べてみた。

形式手法

「テストでは、欠陥が無いことは保証できない」（Edsger W. Dijkstra）
この問題を解決するため、形式手法では、仕様を数学的に記述し、テスト漏れがないことを証明する。
形式手法とモデリング – AlloyAnalyzerを中心に

java -jar "C:\Users\shimizu\Downloads\alloy4.2_2015-02-22.jar"

とすることでAlloy Analyzerが起動した。

試しに1つ実行してみた。

sig User {
	policy : Policy,
}

sig Policy {}

run {}