Better MPA scans and added pickle/JSON output options.

This commit is contained in:
Cas Cremers 2010-12-31 15:43:27 +01:00
parent 9624c49885
commit af25cfc9a0

View File

@ -36,6 +36,7 @@ from Scyther import Scyther
from optparse import OptionParser, OptionGroup, SUPPRESS_HELP from optparse import OptionParser, OptionGroup, SUPPRESS_HELP
import time import time
import os.path import os.path
import json
try: try:
from progressbar import * from progressbar import *
@ -60,6 +61,7 @@ PROTFILETONAME = {}
PROTNAMETOFILE = {} PROTNAMETOFILE = {}
OPTS = None OPTS = None
ARGS = None ARGS = None
PICKLEDATA = set()
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
@ -104,6 +106,8 @@ def parseArgs():
parser.add_option_group(group) parser.add_option_group(group)
# Misc # Misc
parser.add_option("","--pickle",dest="pickle",
help="Do not invoke Scyther but write intended calls to a file with the given name.") # action="store" and type="string" are defaults
parser.add_option("-l","--latex",dest="latex", parser.add_option("-l","--latex",dest="latex",
help="Output latex files with the given prefix.") # action="store" and type="string" are defaults help="Output latex files with the given prefix.") # action="store" and type="string" are defaults
parser.add_option("-v","--verbose",dest="verbose",default=False,action="store_true", parser.add_option("-v","--verbose",dest="verbose",default=False,action="store_true",
@ -162,6 +166,7 @@ class Attack(object):
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
def uniq(l): def uniq(l):
ll = [] ll = []
@ -170,15 +175,36 @@ def uniq(l):
ll.append(x) ll.append(x)
return ll return ll
def powerset(s):
"""
s is a set
returns the powerset
"""
pws = set([frozenset()])
for el in s:
# Double old powerset by adding its elements and also new ones
for s2 in pws.copy():
if len(s2) == 0:
pws.add(frozenset([el]))
else:
pws.add(frozenset([el]).union(s2))
return pws
#--------------------------------------------------------------------------- #---------------------------------------------------------------------------
def MyScyther(protocollist,filt=None,options=[]): def MyScyther(protocollist,filt=None,options=[],checkpickle=True):
""" """
Evaluate the composition of the protocols in protocollist. Evaluate the composition of the protocols in protocollist.
If there is a filter, i.e. "ns3,I1" then only this specific claim If there is a filter, i.e. "ns3,I1" then only this specific claim
will be evaluated. will be evaluated.
By default, when Pickling, no evaluation is done (checkpickle=True).
Setting 'checkpickle' to False ignores this check and verifies anyway.
""" """
global OPTS global OPTS
global PICKLEDATA
s = Scyther.Scyther() s = Scyther.Scyther()
@ -203,8 +229,13 @@ def MyScyther(protocollist,filt=None,options=[]):
if OPTS.debug: if OPTS.debug:
print s.options print s.options
for protocol in protocollist: for protocol in sorted(protocollist):
s.addFile(protocol) s.addFile(protocol)
if checkpickle and OPTS.pickle:
# Do not really verify! Just dump request
PICKLEDATA.add((tuple(sorted(protocollist)),s.options,filt))
else:
# Verify results
s.verifyOne(filt) s.verifyOne(filt)
return s return s
@ -221,7 +252,7 @@ def getCorrectIsolatedClaims(protocolset,options=[]):
goodprotocols = [] goodprotocols = []
if not OPTS.plain: if not OPTS.plain:
widgets = ['Scanning for claims that are correct in isolation: ', Percentage(), ' ', widgets = ['Scanning for claims that are correct in isolation: ', SimpleProgress(), ' protocols (', Percentage(), ') ',
Bar(marker='#',left='[',right=']') Bar(marker='#',left='[',right=']')
] ]
pbar = ProgressBar(widgets=widgets, maxval=len(protocolset)) pbar = ProgressBar(widgets=widgets, maxval=len(protocolset))
@ -230,7 +261,7 @@ def getCorrectIsolatedClaims(protocolset,options=[]):
cpcount = 0 cpcount = 0
for protocol in protocolset: for protocol in protocolset:
# verify protocol in isolation # verify protocol in isolation
s = MyScyther([protocol],options=options) s = MyScyther([protocol],options=options,checkpickle=False)
# investigate the results # investigate the results
goodprotocols.append(protocol) goodprotocols.append(protocol)
allfalse = True allfalse = True
@ -260,9 +291,63 @@ def getCorrectIsolatedClaims(protocolset,options=[]):
return (goodprotocols,correctclaims,cpcount) return (goodprotocols,correctclaims,cpcount)
def verifyProtList(protlist,claimid,options=[]):
"""
Check attacks on this protocol list.
Returns True if no attack ("correct") and False if an attack is found.
"""
s = MyScyther(protlist,claimid,options)
claim = s.getClaim(claimid)
if claim:
if not claim.okay:
return False
return True
def verifyProtSubSet(protlist,claimid,options=[]):
"""
Check attacks on true subsets of this list.
Note subsets must include the claim id
"""
global OPTS
ps = powerset(set(protlist))
for s in ps:
if (len(s) > 0) and (len(s) < len(protlist)):
res = verifyProtList(list(s),claimid,options)
if res == False:
"""
If an attack is found we're actually done but for pickle we
make an exception to generate all possible variants.
"""
if not OPTS.pickle:
return False
return True
def verifyMPAattack(mpalist,claimid,options=[]):
"""
Check for Multi-Protocol Attacks on this protocol list.
Returns True if no attack ("correct") and False if an MPA attack is found.
First consider subsets, so if there is an attack there, don't consider others.
"""
global OPTS
res = verifyProtSubSet(mpalist,claimid,options)
if res or OPTS.pickle:
"""
Only really needed when no attack found but for pickle we make an
exception to generate all possible variants.
"""
return verifyProtList(mpalist,claimid,options)
return True
def verifyMPAlist(mpalist,claimid,options=[]): def verifyMPAlist(mpalist,claimid,options=[]):
""" """
Verify the existence of an attack in this context Check the existence of a multi-protocol attack in this context
If an attack is found, we return False, otherwise True. This is If an attack is found, we return False, otherwise True. This is
needed for the iteration later. needed for the iteration later.
@ -272,14 +357,13 @@ def verifyMPAlist(mpalist,claimid,options=[]):
if OPTS.debug: if OPTS.debug:
print time.asctime(), mpalist, claimid, options print time.asctime(), mpalist, claimid, options
s = MyScyther(mpalist,claimid,options) if not verifyMPAattack(mpalist,claimid,options):
claim = s.getClaim(claimid)
if claim:
if not claim.okay:
global FOUND global FOUND
global ALLFOUND global ALLFOUND
global INVOLVED global INVOLVED
claim = claimidToClaim(claimid)
# This is an MPA attack! # This is an MPA attack!
if OPTS.debug: if OPTS.debug:
print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist)) print "I've found a multi-protocol attack on claim %s in the context %s." % (claimid,str(mpalist))
@ -432,8 +516,9 @@ def findAllMPA(protocolset,options=[],mpaoptions=[]):
# For all these claims... # For all these claims...
if not OPTS.plain: if not OPTS.plain:
widgets = ['Scanning for MPA attacks: ', Percentage(), ' ', widgets = ['Scanning for MPA attacks: ', SimpleProgress(), ' claims (', Percentage(), ') ',
Bar(marker='#',left='[',right=']') Bar(marker='#',left='[',right=']'),
ETA()
] ]
pbar = ProgressBar(widgets=widgets, maxval=len(correct)) pbar = ProgressBar(widgets=widgets, maxval=len(correct))
pbar.start() pbar.start()
@ -730,12 +815,23 @@ def bigTest():
def main(): def main():
global OPTS, ARGS global OPTS, ARGS, PICKLEDATA
(OPTS,ARGS) = parseArgs() (OPTS,ARGS) = parseArgs()
if OPTS.pickle:
PICKLEDATA = set()
bigTest() bigTest()
#simpleTest() #simpleTest()
if OPTS.pickle:
pf = open(OPTS.pickle,"wa")
for el in PICKLEDATA:
json.dump(el,pf)
pf.write("\n")
pf.close()
if __name__ == '__main__': if __name__ == '__main__':
main() main()