(************************************************************* * * * BIND DNS resolver verifier * * * * Samuel Son and Vitaly Shmatikov * * * * * *************************************************************) param redundantHypElim = beginOnly. param traceBacktracking = false. param traceDisplay = long. fun NSt/0. fun At/0. fun CNAMEt/0. fun zeroStage/0. fun oneStage/0. data ValidIP/1. data InvalidIP/1. data ValidDN/1. data InvalidDN/1. data AA/1. data nil/0. data Record/3. reduc GetSrc ( Record( dmnSrc, target, recType ) ) = dmnSrc. reduc GetDst ( Record( dmnSrc, target, recType ) ) = target. reduc GetType ( Record( dmnSrc, target, recType ) ) = recType. reduc GetDnDst ( Record( dmnSrc, ValidDN(target), recType ) ) = target. data Response/4. reduc GetAnswer ( Response( q1, Record(a1,a2,a3), Record(au1,au2,NSt), Record(ad1,ad2,At) ) ) = Record(a1,a2,a3). reduc GetAuth ( Response( q1, Record(a1,a2,a3), Record(au1,au2,NSt), Record(ad1,ad2,At) ) ) = Record(au1,au2,NSt). reduc GetAdd ( Response( q1, Record(a1,a2,a3), Record(au1,au2,Nst), Record(ad1,ad2,At) ) ) = Record(ad1,ad2,At). (* Channels *) free net. data emptyset/0. (* Predicate checking whether it is valid or not *) pred checkrec/1. clauses checkrec: Record( x, InvalidIP(ip), At ); checkrec: Record( x, InvalidDN(dn), NSt ); checkrec: Record( x, InvalidDN(dn), CNAMEt ). pred isInvalid/1. clauses isInvalid:InvalidIP(ip); isInvalid:InvalidDN(dn). data zero/0. data succ/1. pred geq/2. clauses geq:x,x; geq:x,y -> geq:succ(x),y. pred ga/2. clauses ga:succ(x),x; ga:x,y -> ga:succ(x),y. data true/0. data mkName/1. data seedRoot/0. data dnmSeed/0. data cnmSeed/0. data dnmIP/0. data ERRORID0/0. data ERRORID1/0. data ERRORID2/0. data ERRORID3/0. data ERRORID4/0. data ERRORID5/0. data ERRORID6/0. data ERRORID7/0. data ERRORID8/0. data AAFLAG/0. data makeSubName/2. pred isSubName/2. clauses isSubName: x, x; isSubName: makeSubName( z, x ), x; isSubName: x, y -> isSubName: makeSubName( z, x ), y. (* Non-overwritabilities in Section 6.3 for A *) (* query ev: evPoison( At, cached_src_a, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: evInitCache( Record( cached_src_a, cached_dst_a, At), lva ) & ga: lva, lv. ( TRUE: in case, v6,v4 is true, FALSE: in case: v3{E7},v2{E2,E5,E7} ) *) (* Non-overwritabilities in Section 6.3 for CNAME *) (* query ev: evPoison( CNAMEt, cached_src_cname, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ). (Impossible in every case) *) (* Properties in Section 6.4 *) (* query ev: evPoison( NSt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: recursiveQueryStart( y, zone, zone_target ) & isSubName: x, zone & isSubName: y, zone. query ev: evPoison( At, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: recursiveQueryStart( y, zone, zone_target ) & isSubName: x, zone & isSubName: y, zone. query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: recursiveQueryStart( y, zone, zone_target ) & isSubName: x, zone & isSubName: y, zone. *) query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: evInitCache( Record( target, validIP, At), lva ). (* Properties in Section 7.1 *) (* query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: evInitCache( Record( target, validIP, At), lva ). (Other property I want to test) query ev: evPoison( At, cached_src_cname, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ). *) (* Properties in Section 7.2 *) (* query ev: evPoison( At, makeSubName(bad, goddAuth), invalidIP, lv, cached_src_ns, makeSubName(good, goddAuth), cached_src_cname, eid ) ==> ev: evInitCache( Record( makeSubName(good, goddAuth), validIP, At), lva ). query ev: evPoison( At, makeSubName(bad, goddAuth), invalidIP, lv, cached_src_ns, makeSubName(good, goddAuth), cached_src_cname, eid ). ERRORID 0,3,7,2,5 *) (* Properties in Section 7.3 *) (* query ev: evPoison( At, cached_src_a, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: evInitCache( Record( cached_src_a, cached_dst_a, At), lva ) & ga: lva, lv. ( FALSE: in case: v3{E7}, v2{E2,E5,E7} ) *) (* Properties in Section 7.4 *) (* query ev: evPoison( NSt, cached_src_ns, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) ==> ev: evInitCache( Record( cached_src_ns, cached_dst_ns, NSt), lvns ) & ga: lvns, lv. ( FALSE in case any lvns lower than v6: v5{E1},v3{E1},v2{E1,E4} ) *) let processResolver = let v0 = succ(zero) in let v1 = succ(v0) in let v2 = succ(v1) in let v3 = succ(v2) in let v4 = succ(v3) in let v5 = succ(v4) in let v6 = succ(v5) in let v7 = succ(v6) in let v8 = succ(v7) in new currentState; ( ( (* Initialize a cache state. Based on this state, the resolver model makes a decision *) (* At first, the model cache two records: one of them is A type and another is NS type *) new magicZONE; out( net, magicZONE ); (* in ( net, ( initNSlabel, initClabel, initAlabel ) ); *) in ( net, ( makeSubName(NSlabel, =magicZONE), makeSubName(Clabel, =magicZONE), makeSubName(Alabel, =magicZONE) ) ); let initNSlabel = makeSubName(NSlabel, magicZONE) in let initClabel = makeSubName(Clabel, magicZONE) in let initAlabel = makeSubName(Alabel, magicZONE) in let nsRoot = Record( initNSlabel, ValidDN( dnmSeed ), NSt ) in (* Make a NS type record with a domain name and specified IP address *) let aRoot = Record( initAlabel, ValidIP( dnmIP ), At ) in (* Make a A type record with a domain name and specified IP address *) let cnameRoot = Record( initClabel, ValidDN( cnmSeed ), CNAMEt ) in (* In special case for modeling CNAME record in cache *) (* Assert an event declaring cached records with a certain trust levels *) event evInitCache( aRoot, v4 ); (* The trust level of CNAME can be or 6, 4, 3 or 2 *) event evInitCache( nsRoot, v2 ); (* The trust level of CNAME can be or 5, 3 or 2 *) event evInitCache( cnameRoot, v6 ); (* The trust level of CNAME can be or 6 or 4 *) (* currentState is a private internal channel, It is used for passing cached information to resolving process *) out( currentState, ( zeroStage, cnameRoot, aRoot, nsRoot, magicZONE ) ) ) | ( in( currentState, ( =zeroStage, cachedCNAMErecord, cachedArecord, cachedNSrecord, mZONE ) ); (* Get cache information from init process *) !in( net, ( makeSubName(inputname, inputzone), inputtype) ); (* Get a query request from open channel network.*) let input = makeSubName(inputname, inputzone) in event revQuery( input , inputtype ); (* Assert an event that a query arrived *) (*If there is a cached CNAME type record whose label is same as a A type query then, resolution ends*) if ( input, inputtype, GetType(cachedCNAMErecord) ) = ( GetSrc( cachedCNAMErecord ), CNAMEt, CNAMEt ) then ( event queryResolved( input, inputtype ) ) else if ( input, inputtype, GetType(cachedCNAMErecord) ) = ( GetSrc( cachedCNAMErecord ), At, CNAMEt ) then ( (* For CNAMEt, NS section and Additional sections are ignored by BIND resolver *) event queryResolved( input, inputtype ) ) else if ( input, inputtype ) = ( GetSrc( cachedNSrecord ), NSt ) then ( event queryResolved( input, inputtype ) ) (* If there is no record matching to a given query name and type, a recursive query starts. *) else if ( input, inputtype ) <> ( GetSrc( cachedArecord ), GetType( cachedArecord ) ) then ( let srcNSrecord = GetSrc( cachedNSrecord ) in if input = srcNSrecord then out( currentState, ( oneStage, srcNSrecord, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ) else if isSubName: input, srcNSrecord then out( currentState, ( oneStage, srcNSrecord, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ) else if input = mZONE then out( currentState, ( oneStage, mZONE, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ) else if isSubName: input, mZONE then out( currentState, ( oneStage, mZONE, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ) else event resolvingFailed( input ) ) (* if ( input, inputtype ) <> ( GetSrc( cachedArecord ), GetType( cachedArecord ) ) *) else ( event queryResolved( input, inputtype ) ) ) | ( !in( currentState, (=oneStage, srcLabelCachedNS, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ); new dstLabelCachedNS; (* The query must be a subdomain name of zone determined by a resolver, otherwise it'll fail! *) if isSubName: input, srcLabelCachedNS then ( (* Because, there is no data, the model start a recursive query. *) out( net, (input, inputtype) ); event recursiveQueryStart( input, srcLabelCachedNS, dstLabelCachedNS ); (* And now waiting a response from a AA *) in( net, ( Response( =input, b, (*Record( =input, ans_target, =inputtype),*) Record(auth_name, auth_target, =NSt), Record(add_name, add_target, =At) ), aa ) ); let ans = b in let auth = Record( auth_name, auth_target, NSt) in let add = Record( add_name, add_target, At) in (* Let's check the answer section of the response *) if GetSrc(ans) <> nil then ( if (input,inputtype) = (GetSrc(ans),GetType(ans)) then ( if aa = AAFLAG then ( (* Check the validity of reponses. But, in this point, our model resolver has a power to detect the validity of a response. *) if checkrec: ans then event evPoison( GetType(ans), GetSrc(ans), GetDst(ans), v6, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID0 ); if isSubName: GetSrc(auth), srcLabelCachedNS then ( if checkrec: auth then event evPoison( NSt, GetSrc(auth), GetDst(auth), v5, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID1 ) else ( if GetDst(auth) = GetSrc(add) then if isSubName: GetSrc(add), srcLabelCachedNS then if checkrec: add then event evPoison( GetType(add), GetSrc(add), GetDst(add), v2, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID2 ) ) ) (* if isSubName: GetSrc(auth), srcLabelCachedNS then *) ) (* if aa = AAFLAG then *) else (* if a received reponse is not from an authroritative server *) ( if checkrec: ans then event evPoison( GetType(ans), GetSrc(ans), GetDst(ans), v4, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID3 ); if isSubName: GetSrc(auth), srcLabelCachedNS then ( if checkrec: auth then ( if aa <> AAFLAG then event evPoison( NSt, GetSrc(auth), GetDst(auth), v2, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID4 ) ) else ( if GetDst(auth) = GetSrc(add) then if isSubName: GetSrc(add), srcLabelCachedNS then if checkrec: add then event evPoison( GetType(add), GetSrc(add), GetDst(add), v2, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID5 ) ) ) )(* else aa = AAFLAG *) ) (* if input = GetSrc(ans) then *) ) (* if GetSrc(ans) <> nil then *) else if GetSrc(ans) = nil then ( if isSubName: input, GetSrc( auth ) then ( if GetSrc(auth) <> srcLabelCachedNS then ( if isSubName: GetSrc( auth ), srcLabelCachedNS then ( if checkrec: auth then ( event evPoison( NSt, GetSrc(auth), GetDst(auth), v8, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID6 ) ) else (* if checkrec: auth then *) ( (* Here, We cache the received NS record because it is valid! *) if isSubName: GetSrc( add ), srcLabelCachedNS then if GetDst(auth) = GetSrc(add) then if checkrec: add then event evPoison( GetType(add), GetSrc(add), GetDst(add), v3, GetSrc(cachedNSrecord), GetSrc(cachedArecord), GetSrc(cachedCNAMErecord), ERRORID7 ) ) (* if checkrec: auth then *) ) (* if isSubName: GetSrc( auth ), srcLabelCachedNS then *) ) (* if GetSrc(c) <> ZONE *) else (* if GetSrc(c) = ZONE *) ( event NSrecordAlreadyCached( GetSrc(auth) ) ) (* else for if GetSrc(c) <> ZONE *) ) (* isSubName: input, GetSrc(auth) *) ) (* if GetSrc(ans) = nil then *) ) (* if isSubName: input, srcLabelCachedNS then *) else ( (* We have no AA for this query, Therefore, the query is failed. *) event resolvingFailed( input ) ) ) ). process processResolver