class Bpl::CostModeling
Constants
- ADD_LEAK_ANNOTATION_NAME
- EXEMPTIONS
- EXEMPTION_LIST
TODO: This has to refactored – it is copied from shadowing.rb
- INV_VAR_ANNOTATION_NAME
- LEAKAGE_ANNOTATION_NAME
- STUB_ANNOTATION
Public Instance Methods
annotate_function_body!(decl)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 59 def annotate_function_body! decl if (has_annotation?(decl, LEAKAGE_ANNOTATION_NAME)) then decl.body.select{ |s| is_annotation_stmt?(s, LEAKAGE_ANNOTATION_NAME)}.each do |s| value = get_annotation_value s s.insert_after(bpl("$l := $add.i32($l, #{value});")) end else decl.body.select{ |s| s.is_a?(AssumeStatement)}.each do |stmt| next unless values = stmt.get_attribute(:'smack.InstTimingCost.Int64') stmt.insert_after(bpl("$l := $add.i32($l, #{values.first});")) end end end
cost_of(block)
click to toggle source
Iterates over timing annotations of a block and sums them up.
# File lib/bpl/passes/security/cost_modeling.rb, line 76 def cost_of block assumes = block.select{ |s| s.is_a?(AssumeStatement)} cost = assumes.inject(0) do |acc, stmt| if values = stmt.get_attribute(:'smack.InstTimingCost.Int64') acc += values.first.show.to_i end acc end return cost end
exempt?(decl)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 32 def exempt? decl EXEMPTIONS.match(decl) && true end
extract_branches(blocks)
click to toggle source
Given a set of blocks, returns 'GotoStatement's of branches
# File lib/bpl/passes/security/cost_modeling.rb, line 130 def extract_branches blocks branches = [] blocks.each do |block| block.each do |stmt| case 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) end branches.push(stmt) end end end return branches end
extract_control_blocks(head, blocks, cfg)
click to toggle source
Given a loop, this function returns a tuple containing the loop's control blocks and its (unique) exit block.
# File lib/bpl/passes/security/cost_modeling.rb, line 91 def extract_control_blocks(head, blocks, cfg) # Find the last control block, i.e. the block that has a successor that is not in the loop. last_control_block = nil blocks.each do |b| cfg.successors[b].each do |succ| next if blocks.include?(succ) # The last control block has to be unique. raise StandardError if last_control_block last_control_block = b end end # The control block's succesor that is not in the loop is the unique exit block. exit_block = cfg.successors[last_control_block].select{|b| !blocks.include?(b)} raise StandardError unless exit_block.size == 1 # In the case of a simple control statement, the last control block is the head block # and there are no other control blocks. return [last_control_block], exit_block if last_control_block == head # If the loop has a complicated control statement, there will be multiple control # blocks. Identify them all the way up to the head block. work_list = [last_control_block] control_blocks = [last_control_block] until work_list.empty? cfg.predecessors[work_list.shift].each do |pred| next if control_blocks.include?(pred) next if pred == head && (control_blocks.push(pred) || true) control_blocks.push(pred) work_list |= [pred] end end return control_blocks, exit_block end
get_annotation_value(annotationStmt)
click to toggle source
the annotation should have one argument, and we just want whatever it is
# File lib/bpl/passes/security/cost_modeling.rb, line 54 def get_annotation_value annotationStmt raise "annotation should have one argument" unless annotationStmt.arguments.length == 1 return annotationStmt.arguments.first.to_s end
has_annotation?(decl, annot_name)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 48 def has_annotation?(decl, annot_name) return false unless decl.body return (not (decl.body.select{|r| is_annotation_stmt?(r,annot_name)}.empty?)) end
insert_user_leakage!(decl)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 250 def insert_user_leakage! decl if (has_annotation?(decl, ADD_LEAK_ANNOTATION_NAME)) then decl.body.select{ |s| is_annotation_stmt?(s, ADD_LEAK_ANNOTATION_NAME)}.each do |s| value = get_annotation_value s s.insert_after(bpl("assume {:smack.InstTimingCost.Int64 #{value}} true;")) s.remove end end end
is_annotation_stmt?(stmt, annot_name)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 43 def is_annotation_stmt? (stmt, annot_name) return false unless stmt.is_a?(CallStatement) return stmt.procedure.to_s == annot_name end
redirect_to_stub!(decl)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 237 def redirect_to_stub! decl args, asmt = [], [] decl.parameters.each {|d| args.push(d.names.flatten).flatten} decl.returns.each {|d| asmt.push(d.names.flatten).flatten} args, asmt = args.flatten, asmt.flatten stub_name = decl.specifications.first.get_attribute(STUB_ANNOTATION)&.first&.first stub_call = bpl("call #{asmt.join(",")} := #{stub_name}(#{args.join(",")});") myblock = Block.new(names: [], statements: [stub_call]) decl.body.replace_children(:locals, []) decl.body.replace_children(:blocks, myblock) end
run!(program)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 260 def run! program # add cost global variable program.prepend_children(:declarations, bpl("var $l: int;")) program.prepend_children(:declarations, bpl("var $__delta: int;")) # update cost global variable program.each_child do |decl| next unless decl.is_a?(ProcedureDeclaration) next if exempt?(decl.name) next unless decl.body decl.add_attribute(:cost_modeling) redirect_to_stub!(decl) if stub?(decl) if decl.has_attribute?(:entrypoint) decl.body.blocks.first.statements.first.insert_before(bpl("$l := 0;")) end insert_user_leakage! decl summarize_loops! decl annotate_function_body! decl end end
stub?(decl)
click to toggle source
# File lib/bpl/passes/security/cost_modeling.rb, line 24 def stub? decl decl.specifications.each.any? { |s| s.has_attribute? STUB_ANNOTATION } end
summarize_loops!(decl)
click to toggle source
This function automatically computes and inserts leakage-related loop invariants. The invariants are of the form: leakage = leakage_before_entering + loop_counter * (loop_body_cost + control_block_cost)
# File lib/bpl/passes/security/cost_modeling.rb, line 157 def summarize_loops! decl cfg = cfg_construction # Identify loop-cost related annotations loop_vars = [] if (has_annotation?(decl, INV_VAR_ANNOTATION_NAME)) then decl.body.select{ |s| is_annotation_stmt?(s, INV_VAR_ANNOTATION_NAME)}.each do |s| value = get_annotation_value s loop_vars.push(value) end end loop_identification.loops.each do |head, blocks| # Only deal with loops that are in the procedure we are processing. loop_is_in_decl = decl.body.blocks.find do |b| b.name == head.name && decl.name == head.parent.parent.name end next unless loop_is_in_decl # Create leakage_before_entering variable and insert right before the loop head. lkg_before_var = decl.body.fresh_var("$loop_l","i32") lkg_before_asn = AssignStatement.new lhs: lkg_before_var, rhs: bpl("$l") entry = cfg.predecessors[head].detect{ |b| !blocks.include?(b) } entry.statements.last.insert_before(lkg_before_asn) # Identify control blocks, body blocks and compute their costs. control_blocks, exit_block = extract_control_blocks(head, blocks, cfg) body_blocks = blocks - control_blocks # Identify non-nested branches, their consequent blocks and their alternative blocks. # TODO: raise error/warning when we encounetr a non-nested branch. gotos = extract_branches body_blocks branches = {} gotos.each do |goto| consequent = goto.identifiers.first.declaration alternative = goto.identifiers.last.declaration branches[goto] = consequent, alternative end straight_line_blocks = body_blocks branches.each_value do |cons, alt| straight_line_blocks -= [cons, alt] end control_cost = control_blocks.inject(0) { |acc, blk| (acc + (cost_of blk)) } straight_line_cost = straight_line_blocks.inject(0) { |acc, blk| (acc + (cost_of blk)) } # Identify the loop_counter variable as the intersection of live variables of the head # block and its predecessor. counter_update_block = cfg.predecessors[head].detect{ |b| blocks.include?(b) } args = decl.declarations.inject([]) { |acc, d| acc << d.idents[0].name } counter = ((liveness.live[head] & liveness.live[counter_update_block]) - args).first cons_inv = "" branches.values.each_with_index do |(cons, alt), idx| cons_cost = cost_of cons #alt_cost = cost_of alt cons_inv += "$sdiv.i32(#{loop_vars[idx]}+ #{counter} - 1,64)*#{cons_cost}" #puts "(#{continuation} - (old+ #{counter} - 1)/64)*#{alt_cost}" end straight_line_inv = "(#{counter}#{' - 1' unless cons_inv.empty?})*(#{straight_line_cost}+#{control_cost})"; #puts "assert ($l == #{lkg_before_var}+#{straight_line_inv}#{' + ' unless cons_inv.empty?}#{cons_inv});" # Compute and insert leakage invariant at the beginning of the head block. head.prepend_children(:statements, bpl("assert ($l == #{lkg_before_var}+#{straight_line_inv}#{' + ' unless cons_inv.empty?}#{cons_inv});")) end end