From 630f6e94597a88341481d235414341f39d3b58c7 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 21 Aug 2008 21:20:16 +0200 Subject: [PATCH] Added large delta-test script. The script runs over all protocol files it can find, and runs it using two different command-line parameters to scyther. If the results differ, the script reports it. The code can use some cleanup, removing e.g. global variables, but it works. --- gui/Scyther/Scyther.py | 7 -- gui/test-delta.py | 181 ++++++++++++++++++++++++++++++++++++ gui/{mpa.py => test-mpa.py} | 0 3 files changed, 181 insertions(+), 7 deletions(-) create mode 100755 gui/test-delta.py rename gui/{mpa.py => test-mpa.py} (100%) diff --git a/gui/Scyther/Scyther.py b/gui/Scyther/Scyther.py index 7970506..2a735ac 100755 --- a/gui/Scyther/Scyther.py +++ b/gui/Scyther/Scyther.py @@ -262,13 +262,6 @@ class Scyther(object): if spdl: os.remove(fni) - # Now if there is no output and no errors, weird things might - # happen, and we report the command used. - if errors == "" and output == "": - errors = "Scyther backend did not yield any output, " - errors += "returning no errors and no output.\n" - errors += "Command: [%s]" % self.cmd - return (output,errors) def sanitize(self): diff --git a/gui/test-delta.py b/gui/test-delta.py new file mode 100755 index 0000000..d2cb25c --- /dev/null +++ b/gui/test-delta.py @@ -0,0 +1,181 @@ +#!/usr/bin/python +""" + Scyther : An automatic verifier for security protocols. + Copyright (C) 2007 Cas Cremers + + This program is free software; you can redistribute it and/or + modify it under the terms of the GNU General Public License + as published by the Free Software Foundation; either version 2 + of the License, or (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. +""" + + +""" + +Example script to show how to perform large-scale tests using the +Scyther Python API (contained in the Scyther subdirectory) + +In this example, we find the differences between two different switch +settings for a large set of protocols. + +The notification triggers if claim lists differ, or when a claim is okay +in one test but not in the other. Hence, we ignore differences between +complete/bounded verification. + +Author: Cas Cremers + + +Define the strings below. + +TEST0 is used for both, TEST1/2 define the difference between +the tests. +""" +#--------------------------------------------------------------------------- + +TEST0 = "" +TEST1 = "--max-runs=1" +TEST2 = "--max-runs=4" + +#--------------------------------------------------------------------------- + +""" Import externals """ +import commands + +#--------------------------------------------------------------------------- + +""" Import scyther components """ +from Scyther import Scyther + +#--------------------------------------------------------------------------- + +def filterProtocol(protocol): + """ + We may want to filter out some protocols. + This function allows that. Return True if it is okay (and should be + included) or False otherwise. + """ + include = True + return include + +def simpleRun(args): + x = Scyther.Scyther() + x.options = args + x.verify() + return x + +def ScytherRes(protocol,args=""): + """ + Run Scyther on a protocol and return a tuple with the + resulting object and claim list. + """ + global TEST0 + + args = "%s %s %s" % (TEST0, args, protocol) + s = simpleRun(args) + return (s,s.claims) + + +def findSameClaim(cl,claim): + """ + Find in claim list the claim that corresponds to claim + """ + for claim2 in cl: + if claim2.id == claim.id: + return claim2 + return None + + +def ScytherDiff(protocol): + """ + Check whether the two different switch settings yield a different + result. + """ + global TEST1, TEST2 + + (s1,cl1) = ScytherRes(protocol,TEST1) + (s2,cl2) = ScytherRes(protocol,TEST2) + + res = "" + if len(cl1) != len(cl2): + res += "Different claim lists:\n%s\n%s\n" % (cl1,cl2) + else: + for claim1 in cl1: + claim2 = findSameClaim(cl2,claim1) + if claim2 == None: + res += "%s not in second test.\n" % (claim1) + else: + if claim1.okay != claim2.okay: + res += "Different results:\n%s\n%s\n" % (claim1,claim2) + + if res == "": + return None + else: + return res + + +def findProtocols(): + """ + Find a list of protocol names + """ + + cmd = "find -iname '*.spdl'" + plist = commands.getoutput(cmd).splitlines() + nlist = [] + for prot in plist: + if filterProtocol(prot): + nlist.append(prot) + return nlist + + +def main(): + """ + Simple test case with a few protocols + """ + global TEST0,TEST1,TEST2 + + list = findProtocols() + print "Performing delta analysis" + print + print "String 0 (used for both): '%s'" % TEST0 + print "String 1: '%s'" % TEST1 + print "String 2: '%s'" % TEST2 + print + print "After filtering, we are left with the following protocols:", list + print + maxcount = len(list) + count = 1 + delta = 0 + for prot in list: + perc = (100 * count) / maxcount + print "[%i%%] %s: " % (perc,prot), + res = ScytherDiff(prot) + if res != None: + print + print "-" * 72 + print prot + print "-" * 72 + print res + delta = delta + 1 + else: + print "No interesting delta found." + count = count + 1 + + print + print "Analysis complete." + print "%i out of %i protocols differed [%i%%]." % (delta,maxcount,(100 * delta)/maxcount) + + +if __name__ == '__main__': + main() + + +# vim: set ts=4 sw=4 et list lcs=tab\:>-: diff --git a/gui/mpa.py b/gui/test-mpa.py similarity index 100% rename from gui/mpa.py rename to gui/test-mpa.py