JAWS DAYS 2018 に参加した (1)

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

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

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

形式手法

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

モデル検査機 Alloy

Alloy Analyzerをダウンロードして

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

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

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

sig User {
	policy : Policy,
}

sig Policy {}

run {}

コメントを残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です

CAPTCHA


このサイトはスパムを低減するために Akismet を使っています。コメントデータの処理方法の詳細はこちらをご覧ください