Commit 8153c169 authored by Luc Libralesso's avatar Luc Libralesso
Browse files

add model without diff

parent 039dd00d
......@@ -91,6 +91,8 @@ class Minizinc < Backend
# "[|#{joined}|]"
# when Array1D_Value
# "[#{e.array.join(",")}]"
when DiffExpr
"(#{visit(e.a)} != #{visit(e.b)})"
when Operator
e.operator.to_s
when Type
......
......@@ -124,6 +124,21 @@ class Equals < Operation
end
end
class DiffOp < Operation
def initialize(*parameters)
super(Operator.new("!="), *parameters)
end
end
class DiffExpr < Operation
attr_accessor :a, :b
def initialize(a,b)
@a = a
@b = b
super(Priority.new(DiffOp.new(a,b)))
end
end
## TableSum
#
# @param table table to be summed
......
......@@ -12,9 +12,42 @@ require "pry"
class TestWriterGraphviz < Minitest::Unit::TestCase
def test_a()
dag = Midori128_Dag.new(nb_rounds = 4)
model = get_abstract_constraint_model(dag)
file = File.open("test.mzn", "w")
# create dag
nb_rounds = 4
dag = Midori128_Dag.new(nb_rounds = nb_rounds)
# shave dag
atoms,operators = *shave_dag(dag.atoms, dag.operators)
# create initial model
model,variable_dict,xor_clauses = *create_abstract_model(
atoms,
operators,
# "solve minimize obj"
"constraint obj=#{nb_rounds}; solve satisfy"
)
# add diff variables
xor_clauses = xor_clauses + add_diff_variables_mixcolumn_lines(model, atoms, operators, variable_dict)
# add midori128 specific constraints
mc_operators = operators.filter{|op| op.class <= MixColumnsOperator}
mc_operators.each do |op|
model.add_constraints(Diff1.new(variable_dict[op.outputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[1]], variable_dict[op.inputs[0]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[2]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[3]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[1]], variable_dict[op.inputs[0]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[2]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[3]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]]]))
end
# generate new xor clauses and add them to the model
puts("ADDING XOR CLAUSES")
puts("\tstarting with #{xor_clauses.length} clauses")
xor_clauses = generate_xors(atoms, operators, xor_clauses)
puts("\tnow having: #{xor_clauses.length} clauses")
xor_clauses.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
file = File.open("test#{nb_rounds}.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
file.close
assert_equal(true, true)
......
#!/usr/bin/ruby
require_relative "../../cryptodag.rb"
require_relative "../../cryptosystems/midori128/midori128.rb"
require_relative "../../writers/abstract_constraints_without_diff.rb"
require_relative "../../backends/minizinc"
require "minitest/autorun"
# require "minitest/color"
require "pry"
class TestWriterGraphviz < Minitest::Unit::TestCase
def test_a()
# create dag
nb_rounds = 4
dag = Midori128_Dag.new(nb_rounds = nb_rounds)
# shave dag
atoms,operators = *shave_dag(dag.atoms, dag.operators)
# create initial model
model,variable_dict,xor_clauses = *create_abstract_model_without_diffs(
atoms,
operators,
# "solve minimize obj"
"constraint obj=#{nb_rounds}; solve satisfy"
)
# add diff variables
xor_clauses = xor_clauses + add_diff_variables_mixcolumn_lines(model, atoms, operators, variable_dict)
# add midori128 specific constraints
mc_operators = operators.filter{|op| op.class <= MixColumnsOperator}
mc_operators.each do |op|
model.add_constraints(Diff1.new(variable_dict[op.outputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[1]], variable_dict[op.inputs[0]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[2]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[3]]))
model.add_constraints(Diff1.new(variable_dict[op.outputs[3]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[1]], variable_dict[op.inputs[0]], variable_dict[op.inputs[2]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[2]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[3]]]))
xor_clauses.push(Set.new([variable_dict[op.outputs[3]], variable_dict[op.inputs[0]], variable_dict[op.inputs[1]], variable_dict[op.inputs[2]]]))
end
# generate new xor clauses and add them to the model
puts("ADDING XOR CLAUSES")
puts("\tstarting with #{xor_clauses.length} clauses")
xor_clauses = generate_xors(atoms, operators, xor_clauses)
puts("\tnow having: #{xor_clauses.length} clauses")
xor_clauses.each do |xor|
model.add_constraints(Diff1.new(*(xor.map{|v| variable_dict.fetch(v,v)})))
end
file = File.open("testw#{nb_rounds}.mzn", "w")
file.puts(Minizinc.new.generate_code(model))
file.close
assert_equal(true, true)
end
end
......@@ -329,6 +329,7 @@ def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable
ids_to_op[id] = op
id += 1
end
puts "#{mc_operators.length} MIX_COLUMNS OPERATORS"
puts "ADD_DIFF (MIXCOLUMN LINES)"
puts "\t#{mc_operators.length} mixColumns operators found"
diffs = []
......
require 'union_find'
require_relative '../cryptodag.rb'
require_relative '../operators/elementary.rb'
require_relative '../constraints/all.rb'
require_relative './graphviz_atomic.rb'
### DIRTY HACK (modify union_find datastructure)
class UnionFind::UnionFind
public :find_root
end
##############
def shave_dag(atoms, operators)
return *shave_equalities(
*shave_simple_input_xor(
*shave_constants_dag(
*shave_end_dag(
atoms,operators
)
)
)
)
end
##
# simplifies the dag by removing equalities
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_equalities(atoms, operators)
union_find = UnionFind::UnionFind.new(Set.new(atoms))
untouched_atoms = Set.new(atoms)
operators.filter{|op| op.class <= EqualityOperator}.each do |op|
union_find.union(op.inputs[0], op.outputs[0])
untouched_atoms.delete(op.inputs[0])
untouched_atoms.delete(op.outputs[0])
end
old_to_root = {}
root_set = Set.new()
atoms.each do |a|
root_set.add(union_find.find_root(a))
old_to_root[a] = union_find.find_root(a)
end
raise "union find: inconsistent results" unless root_set.length == union_find.count_isolated_components
root_to_new = {}
new_atoms = []
root_set.each do |a|
new_a = Variable.new(a.name, 0..1, value=a.value)
root_to_new[a] = new_a
new_atoms.push(new_a)
end
puts "ELIMINATE EQUALITIES (vars: #{atoms.length} -> #{new_atoms.length})"
# define operators
new_operators = []
operators.filter{|op| !(op.class <= EqualityOperator)}.each do |op|
res = op.dup
res.inputs = op.inputs.map{|a| root_to_new[old_to_root[a]]}
res.outputs = op.outputs.map{|a| root_to_new[old_to_root[a]]}
raise "shave_equalities: different size between new and old input op #{res.inputs.length} should be #{op.inputs.length}" unless res.inputs.length == op.inputs.length
raise "shave_equalities: different size between new and old outputs op" unless res.outputs.length == op.outputs.length
res.inputs.each do |a|
raise "atom non existing in new_atoms set (input of #{res}, #{a})" unless Set.new(new_atoms).include?(a)
end
new_operators.push(res)
end
return [new_atoms, new_operators]
end
##
# returns new xors that can be used to improve the relaxations
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def generate_xors(atoms, operators, custom_xors, max_size=4)
initial_xors = Set.new(operators.filter{|op| op.class <= XorOperator}.map{|op| Set.new(op.inputs+op.outputs)}+custom_xors)
new_xors = initial_xors.dup
variables = Set.new()
variable_adj = {}
new_xors.each do |op|
op.each do |v|
variables.add(v)
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(op)
end
end
xor_to_check = new_xors.dup
puts "GENERATE_XORS(limit=#{max_size}): with #{new_xors.length} initial xors"
to_continue = true
while to_continue
to_continue = false
new_xor_to_check = Set.new()
variables.each do |v|
variable_adj[v].each do |a|
if xor_to_check.include?(a)
variable_adj[v].each do |b|
if a != b
c = (a+b)-(a&b)
if c.length >= 1 && c.length <= max_size
nb_diffs = c.filter{|v| v.name.name.start_with?("diff_")}.length
if nb_diffs <= 1 && !new_xors.include?(c)
new_xors.add(c)
new_xor_to_check.add(c)
to_continue = true
c.each do |v|
variable_adj[v] = variable_adj.fetch(v, Set.new()).add(c)
end
end
end
end
end
end
end
end
xor_to_check = new_xor_to_check
puts "\tround finished with: #{new_xors.length} clauses"
end
return new_xors
end
##
# removes operators and atoms to be shaved and returns a new dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @param to_shave [Set<CryptoAtom|CryptoOperator>]
# @return [new_atoms, new_operators]
def get_dag_subset(atoms, operators, to_shave)
# create new dag with shaved nodes
atom_map = {}
new_atoms = []
# create new set of atoms
atoms.each do |atom|
if !to_shave.include?(atom)
new_atom = Variable.new(atom.name, 0..1, value=atom.value)
atom_map[atom] = new_atom
new_atoms.push(new_atom)
end
end
# create new set of operators
new_operators = []
operators.each do |op|
if !to_shave.include?(op)
new_inputs = op.inputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_outputs = op.outputs.filter{|e| !to_shave.include?(e)}.map{|e| atom_map[e]}
new_op = op.dup
# p "#{op.class <= XorOperator}\t#{new_inputs.length}"
if (op.class <= XorOperator) && (new_inputs.length == 1)
# p "###"
raise "get_dag_subset: node with multiple outputs detected #{op}" unless new_outputs.length == 1
new_op = EqualityOperator.new(new_inputs[0], new_outputs[0])
else
new_op.inputs = new_inputs
new_op.outputs = new_outputs
end
new_operators.push(new_op)
end
end
return [new_atoms, new_operators]
end
##
# simplifies the dag
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_simple_input_xor(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes with 1 output which is a xor
inputs = atoms.filter do |n|
preds.fetch(n, []).length == 0 &&
succs.fetch(n, []).length == 1 &&
succs.fetch(n, [])[0].class <= XorOperator
end
# for each input, replace the xor by
to_shave = Set.new()
inputs.each do |atom|
to_shave.add(atom)
to_shave.add(succs[atom][0])
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes constants from the input nodes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_constants_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
constants = atoms.filter{ |n| n.value != nil }
to_shave = Set.new() # nodes to remove in the shaved model
constants.each do |c|
to_shave.add(c)
end
return get_dag_subset(atoms, operators, to_shave)
end
##
# removes end operators and atoms before S-boxes
# @param atoms [Vec<CryptoAtom=Variable>]
# @param operators [Vec<CryptoOperators>]
# @return [new_atoms, new_operators]
def shave_end_dag(atoms, operators)
# compute precedence and successors relations
preds, succs = *compute_precedences(atoms, operators)
# get input nodes (should be CryptoAtoms)
outputs = atoms.filter{ |n| succs.fetch(n, []).empty? }
to_shave = Set.new() # nodes to remove in the shaved model
outputs.each do |output_atom|
if preds[output_atom].length == 0
to_shave.add(output_atom)
elsif preds[output_atom].length == 1
op = preds[output_atom][0]
# if op is not a SOperator and has only one output, the atom (and operator) can be shaved
if !(op.class <= SOperator) && (succs[op].length == 1)
to_shave.add(output_atom)
to_shave.add(op)
end
else
raise "shave_end_dag: output #{output_atom.name.name} has too many preds (#{preds[output_atom]} should be <= 1)"
end
end
return get_dag_subset(atoms, operators, to_shave)
end
def compute_precedences(atoms, operators)
preds = {}
succs = {}
operators.each do |op|
op.inputs.each do |inp|
preds[op] = preds.fetch(op, []).push(inp)
succs[inp] = succs.fetch(inp, []).push(op)
end
op.outputs.each do |out|
preds[out] = preds.fetch(out, []).push(op)
succs[op] = succs.fetch(op, []).push(out)
end
end
return [preds, succs]
end
def create_abstract_model_without_diffs(atoms, operators, solve_instructions)
model = Model.new()
variable_dict = {} # Atom -> Variable
# add atoms as booleans
atoms.each do |atom|
var = Variable.new(atom.name, 0..1, atom.value != nil ? 0 : nil)
variable_dict[atom] = var
model.add_variables(var)
end
# add constraints
xor_clauses = []
operators.each do |op|
case op.class.name
when "XorOperator"
model.add_constraints(Diff1.new(
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
))
xor_clauses.push(Set.new(
op.inputs.map {|atom| variable_dict[atom]}+
op.outputs.map {|atom| variable_dict[atom]}
))
when "SOperator"
model.add_constraints(Equality.new(
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
))
when "EqualityOperator"
model.add_constraints(Equality.new(
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
))
when "MixColumnsOperator"
model.add_constraints(IncludedIn.new(
Sum.new(
*op.inputs.map {|atom| variable_dict[atom]},
*op.outputs.map {|atom| variable_dict[atom]}
),
Set[0,4,5,6,7,8]
))
model.add_constraints(Equivalence.new(
Equals.new(Sum.new(*op.inputs.map {|atom| variable_dict[atom]}), 0),
Equals.new(Sum.new(*op.outputs.map {|atom| variable_dict[atom]}), 0)
))
else
# p c.class
raise "gen_abstract_constraint_model: unknown operator: #{op.class.name}"
end
end
# add objective function
s_operators = operators.filter {|op| op.class <= SOperator}
obj = Variable.new("obj", 1..64)
model.add_variables(obj)
model.add_constraints(
Equality.new(
obj,
Sum.new(*s_operators.map{|op| variable_dict[op.outputs[0]]})
)
)
model.add_instructions(Instruction.new(solve_instructions))
return [model,variable_dict,xor_clauses]
end
##
#
#
def add_diff_variables_mixcolumn_lines(model, atoms, operators, atom_to_variable)
res_xors = []
mc_operators = operators.filter{|op| op.class <= MixColumnsOperator}
op_to_ids = {}
ids_to_op = {}
id = 0
mc_operators.each do |op|
op_to_ids[op] = id
ids_to_op[id] = op
id += 1
end
puts "#{mc_operators.length} MIX_COLUMNS OPERATORS"
puts "ADD_DIFF (MIXCOLUMN LINES)"
puts "\t#{mc_operators.length} mixColumns operators found"
diffs = []
mc_operators.each do |o1|
mc_operators.each do |o2|
if op_to_ids[o1] < op_to_ids[o2]
4.times do |row|
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"I"])
diffs.push([op_to_ids[o1],op_to_ids[o2],row,"O"])
end
end
end
end
# add mix columns property (sum diffs input + diffs output) for each couple of operators
mc_operators.each do |o1|
mc_operators.each do |o2|
if op_to_ids[o1] < op_to_ids[o2]
exprs_in = 4.times.map{|i| DiffExpr.new(atom_to_variable[o1.inputs[i]], atom_to_variable[o2.inputs[i]])}
exprs_out = 4.times.map{|i| DiffExpr.new(atom_to_variable[o1.outputs[i]], atom_to_variable[o2.outputs[i]])}
model.add_constraints(IncludedIn.new(
Sum.new(
*(exprs_in + exprs_out)
), Set[0,4,5,6,7,8]
))
model.add_constraints(Equivalence.new(
Equals.new(Sum.new(*exprs_in), 0),
Equals.new(Sum.new(*exprs_out), 0)
))
end
end
end
return res_xors
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment