HITCON CTF 2015 risky

HITCON CTF 2015 risky

My team found the binary in question was for RISC-V. I just wrote a
translator from objdump output to equations which should be
satisfied. Another team member got the flag with my result and z3.

parse_risky.rb

puts 's1=a[2]'
puts 's5=a[3]'
puts 's3=a[0]'
puts 's2=a[1]'
puts 's0=a[4]'

rui = nil
ui = nil

`#{ENV['HOME']}/tmp/riscv/toolchain/bin/riscv64-unknown-elf-objdump -S risky` =~ /800684.*?\n(.*?)\n\s+800810/m
$1.each_line do |line|
  toks = line.split[2..-1]
  a = toks[1]
  case toks[0]
  when 'jal'
    if line !~ /(printf|fflush|sleep|putchar)/
      raise line
    end
    #STDERR.puts "ignore: #{line}"
  when 'li'
    if a.split(',')[0] != 'a0'
      puts a.sub(',', '=')
    end
  when 'mulw'
    puts a.sub(',', '=').sub(',', '*')
  when 'lui'
    #puts a.sub(',', '=') + '<<12'
    rui, ui = *a.split(",")
  when 'addiw'
    #puts a.sub(',', '=').sub(',', '+')
    r, r2, i = *a.split(",")
    if r != rui || r != r2
      raise line
    end
    v = (ui.hex << 12) + i.to_i
    puts "#{r}=0x%x" % v
    rui = nil
    ui = nil
  when 'addw'
    puts a.sub(',', '=').sub(',', '+')
  when 'bne'
    puts 'assert(' + a.sub(',', '==').sub(/,.*/,'') + ')'
  else
    raise "#{toks[0]} (#{line})"
  end
end

__END__

s1=a[2]
s5=a[3]
s3=a[0]
s2=a[1]
s0=a[4]
s6=s1*s5
a4=0x181a9c5f
a5=s3*s2
a5=a5+s6
a5=a5+s0
assert(a5==a4)
a5=s3*s1
a4=s2+s0
a5=a5+a4
a4=0x2deacccb
assert(a5==a4)
a5=s3+s2
a5=a5+s1
a5=a5+s5
a5=a5+s0
a4=0x8e2f6780
assert(a5==a4)
s4=s2+s1
s4=s4+s0
a4=s3+s5
a4=a4*s4
a5=0xb3da7b5f
assert(a4==a5)
a5=0xe3b0cdef
assert(s4==a5)
a4=s3*s0
a5=0x4978d844
assert(a4==a5)
s4=s2*s1
a5=0x9bcd30de
assert(s4==a5)
s4=s6*s4
a5=0x41c7a3a0
s4=s4*s0
assert(s4==a5)
a5=0x313ac784
assert(s6==a5)