changeset 104:874e71d7aa8c

bad_call.py tests for illegal calls, secret_ifs are iteratively expanded in ideal_functionality.py
author Sigurd Meldgaard <stm@daimi.au.dk>
date Fri, 10 Jul 2009 13:25:40 +0200
parents 7f816d773350
children 47d11f038cd4
files pysmcl/bad_calls.py pysmcl/flow.py pysmcl/ideal_functionality.py pysmcl/secret_annotator.py pysmcl/secret_ifs.py pysmcl/test/unit/test_secret_ifs.py
diffstat 6 files changed, 61 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/pysmcl/bad_calls.py	Fri Jul 10 13:25:40 2009 +0200
@@ -0,0 +1,19 @@
+import util
+import ast
+from secret_annotator import expr_secret, non_compromising_functions
+
+
+def bad_calls(function_def):
+    for node in ast.walk(function_def):
+        if isinstance(node, ast.stmt):
+            e = node.out_values["secret"]
+        if(isinstance(node, ast.Call)):
+            if(not isinstance(node.func, ast.Name)):
+                if(any([expr_secret(i, e) for i in node.args])):
+                    util.error("Call of non-fixed function \
+with secret argument", node)
+            elif(node.func.id in non_compromising_functions):
+                return
+            elif(any([expr_secret(i, e) for i in node.args])):
+                util.error("Call of non-secret\
+function with secret argument", node)
--- a/pysmcl/flow.py	Fri Jul 10 11:22:55 2009 +0200
+++ b/pysmcl/flow.py	Fri Jul 10 13:25:40 2009 +0200
@@ -1,26 +1,26 @@
-import inspect
 import ast
 import StringIO
 
 # Import PySMCL packages.
 from pysmcl.pretty_print import PrettyPrinter
-import pysmcl.secret_ifs
 
 from pysmcl.graph import Node
 
+
 def analyze(function, join, combine, key, bottom):
     """
-    Doing a simple intra procedural forward analysis using the iterative worklist
-    algorithm. Parametrized by the functions join and combine, and
-    with the value initial.  The lattice-points are stored in each
-    statement-node in_values and out_values, under the *key*.
+    Doing a simple intra procedural forward analysis using the
+    iterative worklist algorithm. Parametrized by the functions join
+    and combine, and with the value initial.  The lattice-points are
+    stored in each statement-node in_values and out_values, under the
+    *key*.
 
-    function (FunctionDef) The function to analyze
-    join (function) A function which takes a set of nodes to be joined
-    combine (function) A function which implement the least upper bound or
-        the greates lower bound
-    key (String) A string used to index into the out_values dictionary
-    bottom (function) A function which computes the bottom element of the lattice
+    function (FunctionDef) The function to analyze join (function) A
+    function which takes a set of nodes to be joined combine
+    (function) A function which implement the least upper bound or the
+    greates lower bound key (String) A string used to index into the
+    out_values dictionary bottom (function) A function which computes
+    the bottom element of the lattice
     """
     # initialization
     worklist = []
@@ -49,10 +49,9 @@
         """
         Prepares all statements under node for further analysis.
         """
-        #make sure to only do this once
-        if "initialized" in node.__dict__:
-            return
         for child in ast.walk(node):
+            if "initialized" in child.__dict__:
+                continue
             if(isinstance(child, ast.stmt)):
                 # children and parents are used for flow-graph edges
                 child.children = set()
@@ -62,8 +61,10 @@
                 # framework.
                 child.in_values = {"secret" : set(), "range": None}
                 child.out_values = {"secret" : set(), "range": None}
-        node.initialized = True
+                child.initialized = True
 
+    # Todo - edges from function returns...
+    # Neccesary?
     def flow(self, function):
         self.init_statements(function)
         #function.body.append(ast.Pass)
@@ -71,8 +72,6 @@
         function.children = [function.body[0]]
         function.body[0].parents = [function]
         self.flow_body(function.body)
-        # Todo - edges from function returns...
-        # Neccesary?
 
     def make_edge(self, from_nodes, to_node):
         for from_node in from_nodes:
@@ -108,18 +107,19 @@
                 current = set([stm])
         return current
 
-
     def to_dot(self, entry):
         """Returns a pysmcl.graph.Node which is the dot node corresponding to entry.
 
         entry (ast.Expr)
         """
+
         def pretty(ast_node):
             output = StringIO.StringIO()
             printer = PrettyPrinter(output)
             printer.visit(ast_node)
             s = output.getvalue()
             return s.replace('\n', '')
+
         def depth_first(entry):
             node = Node([], pretty(entry))
             processed[entry] = node
--- a/pysmcl/ideal_functionality.py	Fri Jul 10 11:22:55 2009 +0200
+++ b/pysmcl/ideal_functionality.py	Fri Jul 10 13:25:40 2009 +0200
@@ -8,6 +8,7 @@
 import pysmcl.secret_ifs
 import pysmcl.compatibility_check
 import pysmcl.proof_burden
+from pysmcl.bad_calls import bad_calls
 
 def ideal_functionality(f):
     print "ideal"
@@ -19,8 +20,12 @@
     #function_ast.decorator_list.remove[0]
     print "-"*80
     pysmcl.compatibility_check.CompatibilityChecker().visit(function_ast)
+    transform_ifs = pysmcl.secret_ifs.TransformIfs()
+    while not transform_ifs.changed:
+        pysmcl.secret_annotator.secret_analysis(function_ast)
+        t = transform_ifs.visit(function_ast)
     pysmcl.secret_annotator.secret_analysis(function_ast)
-    t = pysmcl.secret_ifs.TransformIfs().visit(function_ast)
+    bad_calls(function_ast)
     t.decorator_list.pop()
 #     pysmcl.proof_burden.proof_burden(t)
     pysmcl.pretty_print.PrettyPrinter().visit(t)
--- a/pysmcl/secret_annotator.py	Fri Jul 10 11:22:55 2009 +0200
+++ b/pysmcl/secret_annotator.py	Fri Jul 10 13:25:40 2009 +0200
@@ -1,17 +1,19 @@
 import util
 import ast
+import pretty_print
 
 # Import PySMCL packages.
 import pysmcl.flow
 
+non_compromising_functions = set(["len", "open", "result",
+                                  "invariant", "precondition"])
+
 
 def expr_secret(exp, secret_variables):
     """
     Returns True if the expression exp should be considered secret
     given that the variables in *secret_variables* are secret.
     """
-    non_compromising_functions = set(["len", "open", "result",
-                                      "invariant", "precondition"])
     if(isinstance(exp, ast.BoolOp)):
         return (expr_secret(exp.values[0], secret_variables)
                  or expr_secret(exp.values[1], secret_variables))
@@ -30,20 +32,10 @@
     elif(isinstance(exp, ast.Num)):
         return False
     elif(isinstance(exp, ast.Call)):
-        if(not isinstance(exp.func, ast.Name)):
-            if(any([expr_secret(i, secret_variables) for i in exp.args])):
-                util.error("Call of non-fixed function with secret argument",
-                           exp)
         if(exp.func.id in non_compromising_functions):
             return False
-        #func = eval(exp.func.id)
-        #if(func.secret):
-        #    return True
-        elif(any([expr_secret(i, secret_variables) for i in exp.args])):
-            util.error("Call of non-secret\
- function with secret argument", exp)
         else:
-            return True # For now
+            return True # but bad_calls will warn us
     elif isinstance(exp, ast.Str):
         return False
     else:
@@ -66,7 +58,6 @@
 
     All other statements just pass their value through.
     """
-    ins
     if(getattr(node, "imported_secrets", False)):
         ins = ins | node.imported_secrets
     if(isinstance(node, ast.Assign)):
@@ -74,6 +65,9 @@
             ins = ins | set([node.targets[0].id])
         else:
             ins = ins - set([node.targets[0].id])
+
+    if(isinstance(node, ast.Expr)):
+           expr_secret(node.value, ins)
     if(isinstance(node, ast.Expr) and
        isinstance(node.value, ast.Call) and
        isinstance(node.value.func, ast.Name) and
@@ -88,4 +82,5 @@
 def secret_analysis(function):
     arguments = set(i.id for i in function.args.args)
     function.body[0].imported_secrets = arguments
-    pysmcl.flow.analyze(function, secret_join, secret_combine, "secret", lambda: set())
+    pysmcl.flow.analyze(function, secret_join,
+                        secret_combine, "secret", lambda: set())
--- a/pysmcl/secret_ifs.py	Fri Jul 10 11:22:55 2009 +0200
+++ b/pysmcl/secret_ifs.py	Fri Jul 10 13:25:40 2009 +0200
@@ -51,7 +51,8 @@
         self.changed = False
 
     def visit_While(self, node):
-        if(pysmcl.secret_annotator.expr_secret(node.test, node.in_values["secret"])):
+        if(pysmcl.secret_annotator.expr_secret(
+                node.test, node.in_values["secret"])):
             error("While is not possible on a secret value", node)
         return node
 
@@ -82,11 +83,11 @@
                                 lineno=node.lineno,
                                 col_offset=node.col_offset))
             for i in all_assigned:
-                then_value = assigned_then.get(i, ast.Name(id=i, 
+                then_value = assigned_then.get(i, ast.Name(id=i,
                                                            lineno=node.lineno,
                                                            col_offset=node.col_offset,
                                                            ctx=ast.Load()))
-                else_value = assigned_else.get(i, ast.Name(id=i, 
+                else_value = assigned_else.get(i, ast.Name(id=i,
                                                            lineno=node.lineno,
                                                            col_offset=node.col_offset,
                                                            ctx=ast.Load()))
--- a/pysmcl/test/unit/test_secret_ifs.py	Fri Jul 10 11:22:55 2009 +0200
+++ b/pysmcl/test/unit/test_secret_ifs.py	Fri Jul 10 13:25:40 2009 +0200
@@ -1,17 +1,13 @@
-
-
 import unittest
 import StringIO
-
-from ast import *
-
-from pysmcl.pretty_print import *
+from ast import parse
+from pysmcl.pretty_print import pprint
 from pysmcl.secret_ifs import TransformIfs
 from pysmcl.secret_annotator import secret_analysis
 
+
 class SecretIfTest(unittest.TestCase):
 
-
     def test_ifs(self):
         expected_result = \
 """def f(x):