class Bpl::Shadowing
Constants
- ANNOTATIONS
combines both VARIABLE_ANNOTATIONS and BLOCK_ANNOTATIONS from ct_annotation.rb
- DEFAULT_ARGS
- DEFAULT_ASSERT
- DEFAULT_ASSERT_POINTS
- DEFAULT_MODE
- EXEMPTIONS
- EXEMPTION_LIST
- MAGICS
- MAGIC_LIST
- TIMING_ANNOTATIONS
Public Instance Methods
accesses(stmt)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 68 def accesses(stmt) Enumerator.new do |y| stmt.each do |expr| next unless expr.is_a?(FunctionApplication) next unless expr.function.is_a?(Identifier) next unless expr.function.name =~ /\$(load|store)/ y.yield expr.arguments[1] end end end
add_assertion!(node, position, expr, type)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 183 def add_assertion!(node, position, expr, type) assertion = case @args_hash[type] when nil, :assert_never nil when :assert_now assertion = bpl_assert(expr) when :assert_shadow_ok assertion = shadow_assert(expr) else raise "unexpected assertion time" end return unless assertion if position == :before node.insert_before(assertion) elsif position == :after node.insert_after(assertion) else raise "bad direction" end end
add_assertions!(proc_decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 350 def add_assertions!(proc_decl) equalities = Set.new annotations = annotated_specifications(proc_decl) # Restrict to equality on public inputs annotations[:public_in].each do |annot| loads(annot).each do |e,f| proc_decl.append_children(:specifications, bpl("requires #{e} == #{f};")) end end # Restrict to equality on public / declassified outputs proc_decl.body.each do |ret| next unless ret.is_a?(ReturnStatement) annotations[:public_out].each do |annot| loads(annot).each do |e,f| add_assertion(ret, :before, "#{e} == #{f}", :public_out_assertion) equalities.add(e) end end annotations[:declassified_out].each do |annot| loads(annot).each do |e,f| ret.insert_before(bpl("assume #{e} == #{f};")) end end end if proc_decl.has_attribute?(:entrypoint) if proc_decl.has_attribute?(:cost_modeling) #this is ugly, but seems to be how to destructure the annotation here if max_leakage = annotations[:__VERIFIER_ASSERT_MAX_LEAKAGE]&.first&.first proc_decl.body.select{|r| r.is_a?(ReturnStatement)}.each do |r| r.insert_before(bpl("assume $l >= $l.shadow;")) r.insert_before(bpl("$__delta := $l - $l.shadow;")); r.insert_before(bpl("assert $l <= ($l.shadow + #{max_leakage});")) end else proc_decl.body.select{|r| r.is_a?(ReturnStatement)}.each do |r| r.insert_before(bpl("$__delta := $l - $l.shadow;")) r.insert_before(bpl("assert $l == $l.shadow;")) end end else proc_decl.body.blocks.first.statements.first.insert_before( bpl("$shadow_ok := true;")) proc_decl.body.select{|r| r.is_a?(ReturnStatement)}. each{|r| r.insert_before(bpl("assert $shadow_ok;"))} end end return equalities end
add_loop_invariants!(proc_decl, arguments, equalities)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 409 def add_loop_invariants!(proc_decl, arguments, equalities) #DSN TODO this might need to be changed for the timing example equality_dependencies = dependent_variables(proc_decl, equalities) pointer_argument_dependencies = dependent_variables(proc_decl, arguments.select{|x| x.is_a?(StorageIdentifier) && x.declaration && x.declaration.type.is_a?(CustomType) && x.declaration.type.name == "ref"}) - equality_dependencies value_argument_dependencies = dependent_variables(proc_decl, arguments.select{|x| x.is_a?(StorageIdentifier) && x.declaration && x.declaration.type.is_a?(CustomType) && x.declaration.type.name != "ref"}) - equality_dependencies - pointer_argument_dependencies loop_identification.loops.each do |head,_| block = proc_decl.body.blocks.find do |b| b.name == head.name && proc_decl.name == head.parent.parent.name end next unless block if proc_decl.has_attribute?(:cost_modeling) block.prepend_children(:statements, bpl("assert {:cost_invariant} ($l == $l.shadow);")) else value_argument_dependencies.each do |x| next unless liveness.live[head].include?(x) block.prepend_children(:statements, bpl("assert {:unlikely_shadow_invariant #{x} == #{shadow x}} true;")) end pointer_argument_dependencies.each do |x| next unless liveness.live[head].include?(x) block.prepend_children(:statements, bpl("assert {:likely_shadow_invariant} #{x} == #{shadow x};")) end equality_dependencies.each do |x| next unless liveness.live[head].include?(x) block.prepend_children(:statements, bpl("assert {:shadow_invariant} #{x} == #{shadow x};")) end block.prepend_children(:statements, bpl("assert {:shadow_invariant} $shadow_ok;")) end end end
add_shadow_variables!(proc_decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 213 def add_shadow_variables!(proc_decl) (proc_decl.parameters + proc_decl.returns).each { |d| d.insert_after(shadow_var_decl(d))} proc_decl.body.locals.each { |d| d.insert_after(shadow_var_decl(d))} if proc_decl.body end
annotated_specifications(proc_decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 175 def annotated_specifications(proc_decl) hash = ANNOTATIONS.map{|ax| [ax,[]]}.to_h proc_decl.specifications.each do |s| hash.keys.each {|ax| hash[ax] << s.get_attribute(ax) if s.has_attribute?(ax)} end hash end
bpl_assert(x)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 48 def bpl_assert(x) bpl("assert #{x};") end
create_wrapper_block(original, shadow)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 489 def create_wrapper_block(original, shadow) args = [] asmt = [] original.parameters.each {|d| args.push(d.names.flatten).flatten} original.returns.each {|d| asmt.push(d.names.flatten).flatten} args=args.flatten asmt=asmt.flatten shadow_args = args.map(&method(:shadow)) shadow_assgts = asmt.map(&method(:shadow)) original_id = ProcedureIdentifier.new({:name =>original.name}) shadow_id = ProcedureIdentifier.new({:name => shadow.name}) c1 = CallStatement.new(procedure: original_id, arguments: args, assignments: asmt) c2 = CallStatement.new(procedure: shadow_id, arguments: shadow_args, assignments: shadow_assgts) r = ReturnStatement.new() Block.new(names: [], statements: [c1,c2,r]) end
cross_product(proc)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 209 def cross_product(proc) end
cross_product_block!(block)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 260 def cross_product_block!(block) equalities = Set.new arguments = Set.new proc_decl = block.parent.parent block.each do |stmt| case stmt when AssumeStatement # TODO should we be shadowing assume statements? # NOTE apparently not; because when they appear as branch # conditions, they make the preceding shadow assertion # trivially true. # stmt.insert_after(shadow_copy(stmt)) # XXX this is an ugly hack to deal with memory intrinsic # XXX functions which are implemented with assume statemnts if magic?(proc_decl.name) stmt.insert_after(shadow_copy(stmt)) end when AssignStatement # ensure the indicies to loads and stores are equal accesses(stmt).each do |idx| add_assertion!(stmt, :before, shadow_eq(idx), :memory_assertion) equalities.add(idx) end # shadow the assignment stmt.insert_after(shadow_copy(stmt)) when CallStatement if magic?(stmt.procedure.name) stmt.arguments.each do |x| unless x.type.is_a?(MapType) if x.any?{|id| id.is_a?(StorageIdentifier)} #DSN: This appears to be to ensure that malloc and free are called with the same args? add_assertion!(stmt, :before, shadow_eq(x), :magic_param_args_assertion) equalities.add(x) end end end end if exempt?(stmt.procedure.name) stmt.assignments.each do |x| stmt.insert_after(bpl("#{shadow(x)} := #{x};")) end else shadow_proc_call!(stmt, "cross_product") stmt.arguments.each do |x| arguments.add(x) x.insert_after(shadow_copy(x)) end stmt.assignments.each do |x| x.insert_after(shadow_copy(x)) end end when HavocStatement nxt = stmt.next_sibling if nxt and nxt.is_a?(AssumeStatement) nxt.insert_after(shadow_copy(nxt)) end stmt.insert_after(shadow_copy(stmt)) when GotoStatement next if stmt.identifiers.length < 2 unless stmt.identifiers.length == 2 fail "Unexpected goto statement: #{stmt}" end if annotation = stmt.previous_sibling fail "Expected :branchcond annotation" unless annotation.has_attribute?(:branchcond) if expr = annotation.get_attribute(:branchcond).first add_assertion!(stmt, :before, shadow_eq(expr), :branchcond_assertion) equalities.add(expr) end end end end return equalities, arguments end
dependent_variables(proc, exprs)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 79 def dependent_variables(proc, exprs) dependencies = Set.new work_list = exprs.to_a.dup covered = Set.new(work_list) until work_list.empty? node = work_list.shift node.each do |id| next unless id.is_a?(StorageIdentifier) next if id.declaration && id.declaration.parent.is_a?(Program) next unless definitions = definition_localization.definitions[proc.name][id.name] dependencies.add(id.name) definitions.each do |stmt| next if covered.include?(stmt) covered.add(stmt) work_list << stmt end end end return dependencies end
exempt?(decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 154 def exempt? decl EXEMPTIONS.match(decl) && true end
full_self_composition(original)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 521 def full_self_composition(original) if original.body shadow = shadow_decl(original) original.insert_after(shadow) if original.has_attribute?(:entrypoint) wrapper = original.copy wrapper.replace_children(:name, "#{original.name}.wrapper") original.remove_attribute(:entrypoint) original.add_attribute(:inline, 1) shadow.remove_attribute(:entrypoint) shadow.add_attribute(:inline, 1) #wrapper already has :entrypoint attribute from cloning # transform entry function to wrapper function that # calls original and shadow entry functions wrapper_block = create_wrapper_block(original, shadow) add_shadow_variables!(wrapper) wrapper.body.replace_children(:locals, []) wrapper.body.replace_children(:blocks, wrapper_block) add_assertions!(wrapper) if @args_hash.has_key?(:verify_stub) remove_call!(original, @args_hash[:verify_stub].to_s.concat("_stub")) remove_call!(shadow, @args_hash[:verify_stub].to_s.concat(".shadow")) end original.insert_after(wrapper) end end end
loads(annotation)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 105 def loads(annotation) load_expr, map_expr, addr_expr, inc_expr, len_expr = annotation Enumerator.new do |y| if map_expr.nil? y.yield( bpl("#{load_expr}"), bpl("#{shadow load_expr}")) elsif len_expr.nil? y.yield( bpl("#{load_expr}(#{map_expr}, #{addr_expr})"), bpl("#{load_expr}(#{shadow map_expr}, #{shadow_copy addr_expr})")) else (len_expr.value / inc_expr.value).times do |i| y.yield( bpl("#{load_expr}(#{map_expr}, #{addr_expr} + #{i * inc_expr.value})"), bpl("#{load_expr}(#{shadow map_expr}, #{shadow_copy addr_expr} + #{i * inc_expr.value})") ) end end end end
magic?(decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 158 def magic? decl MAGICS.match(decl) && true end
parse_args(args)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 16 def parse_args(args) rval = Hash.new args.split(",").each do |a| left,right = a.split("=") #symbols are clearer than strings in code rval[left.to_sym] = right.to_sym end return rval end
remove_call!(decl, proc_name)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 514 def remove_call!(decl, proc_name) decl.body.each do |stmt| next unless stmt.is_a?(CallStatement) stmt.remove if stmt.procedure.name.eql? proc_name end end
run!(program)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 608 def run! program @args_hash = parse_args(argslist) # duplicate global variables program.global_variables.each {|v| v.insert_after(shadow_var_decl(v))} program.prepend_children(:declarations, bpl("var $shadow_ok: bool;")) # duplicate parameters, returns, and local variables program.each_child do |decl| next unless decl.is_a?(ProcedureDeclaration) next if exempt?(decl.name) if @args_hash[:self_comp_mode] == :full full_self_composition(decl) elsif @args_hash[:self_comp_mode] == :selective selective_self_composition(decl) else raise "unknown self comp mode #{@args_hash[:self_comp_mode]}" end end end
selective_self_composition(decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 559 def selective_self_composition(decl) # We need to create three copies of each function, to be called depending on # the conext: # 1. the cross_product copy, called from the cross-product context, # 2. the original copy, called from the selective-self-composition context # 3. the shadow copy, called from the selective-self-composition context. # decl is the original - should not be touched by this function product_decl = decl.copy add_shadow_variables!(product_decl) if product_decl.body equalities = Set.new arguments = Set.new product_decl.body.blocks.each do |block| if ins = self_composition_block!(block) # It is crutial that this be inserted after, because otherwise the entry block might become # accidentally set to the shadow, which would be bad. block.insert_after(ins[:block]) equalities.merge(ins[:eqs]) else eqs, args = cross_product_block!(block) equalities.merge(eqs) arguments.merge(args) end end equalities.merge( add_assertions!(product_decl) ) add_loop_invariants!(product_decl, arguments, equalities) end product_decl.replace_children(:name, "#{decl.name}.cross_product") if decl.has_attribute?(:entrypoint) decl.replace_with(product_decl) else decl.insert_after(product_decl) #shadow is for the shadow calls decl.insert_after(shadow_decl(decl)) if decl.body end end
self_composition_block!(block)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 220 def self_composition_block!(block) return nil unless block.statements.first.has_attribute?(:selfcomp) head, tail = block.statements.first.get_attribute(:selfcomp) shadow_block = shadow_copy(block) equalities = Set.new # replace returns and exits in the original block block.each do |stmt| case stmt when ReturnStatement when GotoStatement if stmt.identifiers.map(&:name).include?(tail) fail "Unexpected branching exit" unless stmt.identifiers.count == 1 else next end else next end stmt.replace_with(bpl("goto #{shadow(head)};")) end shadow_block.replace_children(:names, *shadow_block.names.map(&method(:shadow))) shadow_block.each do |label| next unless label.is_a?(LabelIdentifier) && label.name != tail label.replace_with(LabelIdentifier.new(name: shadow(label.name))) end shadow_block.each do |stmt| next unless stmt.is_a?(AssumeStatement) next unless values = stmt.get_attribute(:branchcond) expr = bpl(unshadow values.first) add_assertion!(stmt, :after, shadow_eq(expr), :self_comp_branch_assertion) equalities.add(expr) end return { block: shadow_block, before: tail, eqs: equalities } end
shadow(x)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 30 def shadow(x) "#{x}.shadow" end
shadow_assert(expr)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 205 def shadow_assert(expr) bpl("$shadow_ok := $shadow_ok && #{expr};") end
shadow_copy(node)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 49 def shadow_copy(node) shadow = node.copy shadow.each do |expr| case expr when StorageIdentifier next if expr.declaration && ( expr.declaration.is_a?(ConstantDeclaration) || expr.declaration.parent.is_a?(QuantifiedExpression) ) expr.name = shadow(expr) when CallStatement next if exempt?(expr.procedure.name) next if magic?(expr.procedure.name) shadow_proc_call!(expr) end end return shadow end
shadow_decl(decl)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 470 def shadow_decl(decl) s_decl = decl.copy s_decl.replace_children(:name, shadow(decl.name)) # shadow global variables s_decl.body.blocks.each do |block| block.each do |expr| if expr.is_a?(Identifier) && expr.is_variable? && expr.is_global? expr.name = shadow(expr) end if expr.is_a?(CallStatement) next if exempt?(expr.procedure.name) shadow_proc_call!(expr) end end end s_decl end
shadow_eq(x)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 32 def shadow_eq(x) "#{x} == #{shadow_copy(x)}" end
shadow_proc_call!(expr, suffix="shadow")
click to toggle source
Shadows the procedure identifier of a CallStatement. Using a String
instead of a ProcedureIntefier object (i.e. by simply shadowing the name) breaks compatibility with any postprocessing of the ast.
# File lib/bpl/passes/security/shadowing.rb, line 41 def shadow_proc_call!(expr, suffix="shadow") #TODO: is there a better way to right this? return if("#{expr.procedure}" == "nondet") procedure_id = ProcedureIdentifier.new(:name => "#{expr.procedure}.#{suffix}") expr.procedure.replace_with(procedure_id) end
shadow_var_decl(v)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 34 def shadow_var_decl(v) v.class.new(names: v.names.map(&method(:shadow)), type: v.type) end
unshadow(x)
click to toggle source
# File lib/bpl/passes/security/shadowing.rb, line 31 def unshadow(x) "#{x}".sub(/[.]shadow\z/,'') end