scyther/gui/Scyther/Scyther.py

531 lines
14 KiB
Python
Raw Normal View History

2006-08-02 13:59:57 +01:00
#!/usr/bin/python
2007-06-11 13:09:24 +01:00
"""
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.
"""
2006-08-02 13:59:57 +01:00
#
# Scyther interface
#
#---------------------------------------------------------------------------
""" Import externals """
import os
import os.path
2006-08-02 13:59:57 +01:00
import sys
import StringIO
import tempfile
try:
import hashlib
HASHLIB = True
except ImportError:
HASHLIB = False
pass
2006-08-02 13:59:57 +01:00
#---------------------------------------------------------------------------
""" Import scyther components """
import XMLReader
2006-12-14 14:06:50 +00:00
import Error
import Claim
2006-08-02 13:59:57 +01:00
from Misc import *
#---------------------------------------------------------------------------
2006-12-14 14:06:50 +00:00
"""
Globals
"""
FirstCheck = True
#---------------------------------------------------------------------------
2006-11-23 11:28:51 +00:00
"""
The default path for the binaries is set in __init__.py in the (current)
directory 'Scyther'.
"""
2006-08-09 10:26:15 +01:00
2006-08-09 12:39:35 +01:00
def setBinDir(dir):
2006-08-09 10:26:15 +01:00
global bindir
bindir = dir
2006-08-09 12:54:37 +01:00
def getBinDir():
global bindir
return bindir
2006-08-09 10:26:15 +01:00
#---------------------------------------------------------------------------
2006-12-14 14:06:50 +00:00
def Check():
"""
Various dynamic checks that can be performed before starting the
backend.
"""
global FirstCheck
# First time
if FirstCheck:
"""
Perform any checks that only need to be done the first time.
"""
FirstCheck = False
# Every time
# Check Scyther backend program availability
program = getScytherBackend()
CheckSanity(program)
2006-12-14 14:06:50 +00:00
#---------------------------------------------------------------------------
def CheckSanity(program):
"""
This is where the existence is checked of the Scyther backend.
"""
if not os.path.isfile(program):
raise Error.BinaryError, program
#---------------------------------------------------------------------------
def EnsureString(x,sep=" "):
"""
Takes a thing that is either a list or a string.
Turns it into a string. If it was a list, <sep> is inserted, and the
process iterats.
TODO does not accept unicode yet, that is something that must be
handled to or we run into wxPython problems eventually.
"""
if type(x) is str:
return x
elif type(x) is list:
newlist = []
for el in x:
newlist.append(EnsureString(el,sep))
return sep.join(newlist)
else:
raise Error.StringListError, x
#---------------------------------------------------------------------------
2006-11-23 11:28:51 +00:00
def getScytherBackend():
# Where is my executable?
#
# Auto-detect platform and infer executable name from that
#
if "linux" in sys.platform:
""" linux """
scythername = "scyther-linux"
elif "darwin" in sys.platform:
2006-08-04 23:00:22 +01:00
""" OS X """
2007-01-09 14:37:17 +00:00
scythername = "scyther-mac"
2006-11-23 11:28:51 +00:00
elif sys.platform.startswith('win'):
2006-11-23 11:28:51 +00:00
""" Windows """
scythername = "scyther-w32.exe"
2006-11-23 11:28:51 +00:00
else:
2006-11-23 11:28:51 +00:00
""" Unsupported"""
2006-12-14 14:06:50 +00:00
raise Error.UnknownPlatformError, sys.platform
2006-11-23 11:28:51 +00:00
program = os.path.join(getBinDir(),scythername)
return program
2006-12-14 19:46:36 +00:00
2006-11-23 11:28:51 +00:00
#---------------------------------------------------------------------------
class Scyther(object):
def __init__ ( self):
2006-08-04 23:00:22 +01:00
2006-08-08 16:54:00 +01:00
# Init
2006-11-23 11:28:51 +00:00
self.program = getScytherBackend()
2006-08-02 13:59:57 +01:00
self.spdl = None
self.inputfile = None
self.filenames = []
2006-08-08 17:16:28 +01:00
self.options = ""
2006-08-02 13:59:57 +01:00
self.claims = None
2006-08-06 20:52:07 +01:00
self.errors = None
2006-08-06 22:16:14 +01:00
self.errorcount = 0
self.warnings = None
2006-08-07 11:52:48 +01:00
self.run = False
2006-08-08 16:54:00 +01:00
self.output = None
self.cmd = None
2006-08-08 16:54:00 +01:00
# defaults
self.xml = True # this results in a claim end, otherwise we simply get the output
2006-08-02 13:59:57 +01:00
def setInput(self,spdl):
self.spdl = spdl
self.inputfile = None
self.guessFileNames()
2006-08-02 13:59:57 +01:00
def setFile(self,filename):
self.inputfile = filename
self.filenames = [self.inputfile]
2006-08-02 13:59:57 +01:00
self.spdl = ""
fp = open(filename,"r")
for l in fp.readlines():
self.spdl += l
fp.close()
def addFile(self,filename):
self.inputfile = None
if not self.spdl:
self.spdl = ""
fp = open(filename,"r")
for l in fp.readlines():
self.spdl += l
fp.close()
self.guessFileNames()
def guessFileNames(self,spdl=None):
"""
Try to extract filenames (well, actually, protocol names) sloppily from some spdl script.
There are two modes:
[init] : If the spdl parameter is empty or None, we reset the filenames and extract from self.spdl
[add] : If the spdl parameter is non-empty, add the extracted filenames to an existing list
"""
if (spdl == None) or (len(spdl) == 0):
spdl = self.spdl
2010-12-31 14:42:01 +00:00
if spdl == None:
spdl = ""
self.filenames = []
for sl in spdl.splitlines():
l = sl.strip()
prefix = "protocol "
postfix = "("
x = l.find(prefix)
if x >= 0:
# The prefix occurs
y = l.find(postfix,x+len(prefix))
if y >= 0:
gn = l[x+len(prefix):y]
# check for helper protocols
if not gn.startswith("@"):
if gn not in self.filenames:
self.filenames.append(gn)
def addArglist(self,arglist):
for arg in arglist:
self.options += " %s" % (arg)
2006-12-14 19:46:36 +00:00
def doScytherCommand(self, spdl, args):
"""
Cached version of the 'real' below
"""
global HASHLIB
if not HASHLIB:
return self.doScytherCommandReal(spdl,args)
# So we have the hashing libs
m = hashlib.sha256()
if spdl == None:
m.update("[spdl:None]")
else:
m.update(spdl)
if args == None:
m.update("[args:None]")
else:
m.update(args)
uid = m.hexdigest()
# Split the uid to make (256?) subdirectories
prefixlen = 2
uid1 = uid[:prefixlen]
uid2 = uid[prefixlen:]
# Possibly we could also decide to store input and arguments in the cache to analyze things later
path = "Cache/%s/" % (uid1)
name1 = "%s.out" % (uid2)
name2 = "%s.err" % (uid2)
fname1 = path + name1
fname2 = path + name2
try:
"""
Try to retrieve the result from the cache
"""
fh1 = open(fname1,"r")
out = fh1.read()
fh1.close()
fh2 = open(fname2,"r")
err = fh2.read()
fh2.close()
return (out,err)
except:
"""
Something went wrong, do the real thing and cache afterwards
"""
(out,err) = self.doScytherCommandReal(spdl,args)
# Store result in cache
ensurePath(path)
fh1 = open(fname1,"w")
fh1.write(out)
fh1.close()
fh2 = open(fname2,"w")
fh2.write(err)
fh2.close()
return (out,err)
def doScytherCommandReal(self, spdl, args):
2006-12-14 19:46:36 +00:00
"""
Run Scyther backend on the input
Arguments:
spdl -- string describing the spdl text
args -- arguments for the command-line
Returns:
(output,errors)
output -- string which is the real output
errors -- string which captures the errors
"""
2006-11-23 11:28:51 +00:00
if self.program == None:
2006-12-14 19:46:36 +00:00
raise Error.NoBinaryError
2006-08-02 13:59:57 +01:00
2006-12-14 20:32:24 +00:00
# Sanitize input somewhat
if spdl == "":
2006-12-14 20:32:24 +00:00
# Scyther hickups on completely empty input
spdl = "\n"
2006-12-14 20:32:24 +00:00
# Extract filenames for error reporting later
self.guessFileNames(spdl=spdl)
# Generate temporary files for the output.
# Requires Python 2.3 though.
(fde,fne) = tempfile.mkstemp() # errors
(fdo,fno) = tempfile.mkstemp() # output
if spdl:
(fdi,fni) = tempfile.mkstemp() # input
# Write (input) file
fhi = os.fdopen(fdi,'w+b')
fhi.write(spdl)
fhi.close()
# Generate command line for the Scyther process
2006-12-14 19:46:36 +00:00
self.cmd = ""
2010-05-15 23:36:06 +01:00
self.cmd += "\"%s\"" % self.program
self.cmd += " --append-errors=%s" % fne
self.cmd += " --append-output=%s" % fno
self.cmd += " %s" % args
if spdl:
self.cmd += " %s" % fni
# Only for debugging, really
##print self.cmd
# Start the process
safeCommand(self.cmd)
# reseek
fhe = os.fdopen(fde)
fho = os.fdopen(fdo)
errors = fhe.read()
output = fho.read()
# clean up files
fhe.close()
fho.close()
os.remove(fne)
os.remove(fno)
if spdl:
os.remove(fni)
2006-12-14 19:46:36 +00:00
return (output,errors)
def sanitize(self):
""" Sanitize some of the input """
self.options = EnsureString(self.options)
def verify(self,extraoptions=None):
2006-12-14 19:46:36 +00:00
""" Should return a list of results """
# Cleanup first
self.sanitize()
2006-12-14 19:46:36 +00:00
# prepare arguments
args = ""
if self.xml:
args += " --dot-output --xml-output --plain"
args += " %s" % self.options
if extraoptions:
# extraoptions might need sanitizing
args += " %s" % EnsureString(extraoptions)
2006-12-14 19:46:36 +00:00
# execute
(output,errors) = self.doScytherCommand(self.spdl, args)
self.run = True
# process errors
self.errors = []
self.warnings = []
2006-12-14 19:46:36 +00:00
for l in errors.splitlines():
line = l.strip()
if len(line) > 0:
# filter out any non-errors (say maybe only claim etc) and count
# them.
if line.startswith("claim\t"):
# Claims are lost, reconstructed from the XML output
pass
elif line.startswith("warning"):
# Warnings are stored seperately
self.warnings.append(line)
else:
# otherwise it is an error
self.errors.append(line)
2006-08-06 22:16:14 +01:00
self.errorcount = len(self.errors)
if self.errorcount > 0:
raise Error.ScytherError(self.errors,filenames=self.filenames,options=self.options)
2006-08-06 20:52:07 +01:00
2006-12-14 19:46:36 +00:00
# process output
self.output = output
self.validxml = False
self.claims = []
2006-08-08 16:54:00 +01:00
if self.xml:
if len(output) > 0:
2006-08-08 17:16:28 +01:00
if output.startswith("<scyther>"):
2006-12-14 19:46:36 +00:00
# whoohee, xml
2006-08-08 17:16:28 +01:00
self.validxml = True
2006-12-14 19:46:36 +00:00
xmlfile = StringIO.StringIO(output)
reader = XMLReader.XMLReader()
self.claims = reader.readXML(xmlfile)
2006-08-02 13:59:57 +01:00
2006-12-14 19:46:36 +00:00
# Determine what should be the result
if self.xml:
return self.claims
else:
return self.output
2006-08-02 13:59:57 +01:00
def verifyOne(self,cl=None):
"""
Verify just a single claim with an ID retrieved from the
procedure below, 'scanClaims', or a full claim object
"""
if cl:
# We accept either a claim or a claim id
if isinstance(cl,Claim.Claim):
cl = cl.id
return self.verify("--filter=%s" % cl)
else:
# If no claim, then its just normal verification
return self.verify()
def scanClaims(self):
"""
Retrieve the list of claims. Of each element (a claim), claim.id
can be passed to --filter=X or 'verifyOne' later.
A result of 'None' means that some errors occurred.
"""
self.verify("--scan-claims")
if self.errorcount > 0:
return None
else:
self.validxml = False # Signal that we should not interpret the output as XML
return self.claims
def getClaim(self,claimid):
if self.claims:
for cl in self.claims:
if cl.id == claimid:
return cl
return None
2006-08-02 13:59:57 +01:00
def __str__(self):
2006-08-07 11:52:48 +01:00
if self.run:
if self.errorcount > 0:
2006-08-07 17:40:46 +01:00
return "%i errors:\n%s" % (self.errorcount, "\n".join(self.errors))
2006-08-07 11:52:48 +01:00
else:
2006-08-08 17:16:28 +01:00
if self.xml and self.validxml:
s = "Verification results:\n"
2006-08-08 16:54:00 +01:00
for cl in self.claims:
s += str(cl) + "\n"
return s
else:
return self.output
2006-08-02 13:59:57 +01:00
else:
return "Scyther has not been run yet."
#---------------------------------------------------------------------------
def GetInfo(html=False):
"""
Retrieve a tuple (location,string) with information about the tool,
retrieved from the --expert --version data
"""
program = getScytherBackend()
arg = "--expert --version"
sc = Scyther()
(output,errors) = sc.doScytherCommand(spdl=None, args=arg)
if not html:
return (program,output)
else:
sep = "<br>\n"
html = "Backend: %s%s" % (program,sep)
for l in output.splitlines():
l.strip()
html += "%s%s" % (l,sep)
return html
2007-10-08 13:52:50 +01:00
def GetLicense():
"""
Retrieve license information.
"""
program = getScytherBackend()
arg = "--license"
sc = Scyther()
(output,errors) = sc.doScytherCommand(spdl=None, args=arg)
return output
#---------------------------------------------------------------------------
2006-12-14 19:46:36 +00:00
# vim: set ts=4 sw=4 et list lcs=tab\:>-: