Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Alloy による AWS セキュリティグループのモデリング
// **************************************************
// AWS セキュリティグループのモデル
// **************************************************
// 通信プロトコル
enum Protocol { TCP, UDP, ICMP }
// 通信ポート
sig Port {}
// IP と CIDR
sig IP {}
sig CIDR {
ips : set IP,
}
// セキュリティグループに設定するルール
abstract sig Rule {
protocol : one Protocol,
ports : set Port,
} {
protocol = ICMP <=> no ports
}
// インバウンドルール
sig InboundRule extends Rule {
source : lone CIDR + SecurityGroup,
}
// アウトバウンドルール
sig OutboundRule extends Rule {
destination : lone CIDR + SecurityGroup,
}
// セキュリティグループ
sig SecurityGroup {
inRules : set InboundRule,
outRules : set OutboundRule,
}
// ルールはセキュリティグループに依存してのみ存在できる
fact noIsolatedRules {
all r : Rule | some (inRules + outRules).r
}
// EC2 インスタンス
sig Instance {
priIPs : some IP,
secGrps : set SecurityGroup,
}
// IP アドレスはたかだか一つのインスタンスのみに紐づく
fact privateIPsAreUnique {
all ip : IP | lone priIPs.ip
}
// インバウンドルールが許可されている
pred inboundOK(src, dest : Instance, proto : Protocol, port : Port) {
some r : dest.secGrps.inRules
| proto = r.protocol &&
port in r.ports &&
some (src.priIPs & r.source.ips) +
(src.secGrps & r.source)
}
// アウトバウンド通信が許可されている
pred outboundOK(src, dest : Instance, proto : Protocol, port : Port) {
some r : src.secGrps.outRules
| proto = r.protocol &&
port in r.ports &&
some (dest.priIPs & r.destination.ips) +
(dest.secGrps & r.destination)
}
// インスタンス i1, i2 間で通信が成立する設定の具体例を探索
run {
some disj i1, i2 : Instance, proto : Protocol, port : Port
| inboundOK[i1, i2, proto, port] &&
outboundOK[i1, i2, proto, port]
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment