Alloy による AWS セキュリティグループのモデリング

alloy_aws_security_group.als

// **************************************************
//  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]
}