softsec-kaist / meandiff Goto Github PK

View Code? Open in Web Editor NEW

77.0 11.0 11.0 378 KB

Testing Intermediate Representations for Binary Analysis (ASE '17)

Home Page: https://softsec-kaist.github.io/MeanDiff/

License: MIT License

F# 99.07% Makefile 0.57% Shell 0.36%

differential-testing semantic-bugs symbolic-execution fsharp binary-analysis

meandiff's People

Contributors

Stargazers

Watchers

Forkers

techlord-rce idkwim chubbymaggie ufwt dimas3452 fuzzamos ajaymas pombredanne hhao020 yongwoo36

meandiff's Issues

Invalid padding - `mov`

Description

When moving segment register (two bytes), for instance ES, to register (four bytes), it is invalidly padded. According to the Intel manual, "When executing MOV Reg, Sreg, the processor copies the content of Sreg to the 16 least significant bits of the
general-purpose register. The upper bits of the destination register are zero for most IA-32 processors [...]"

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-35

Affected instructions:

0x8cc0    # mov
0x8cc8

Reproduction guide

Instruction:

00000000  8CC0              mov eax,es

Input:

binsec disasm -decode 8cc0

Observed output:

mov ax, es ⎧1: eax{0, 15} := es₍₁₆₎
           ⎩2: goto ({0x00000002; 32}, 0)

Expected output:
EAX set with correct paddding.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Test Remill semantics

Description

Remill is a library that lifts x86, amd64 (x87, mmx, sse, avx), and aarch64 instructions to LLVM IR. I can provide some assistance if you're interested.

Unable to recognize prefix - `mov`, `lea`

Description

Fails to correctly decode prefix and use correct operand sizes.

Reference:
mov: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-35
lea: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-528

Affected instructions:

0x6689c8    # mov
0x668d0400  # lea

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  6689C8            mov ax,cx

Input:

binsec disasm -decode 6689c8

Observed output:

mov eax, ecx ⎧1: eax := ecx₍₃₂₎
             ⎩2: goto ({0x00000003; 32}, 0)

Expected output:
Correctly decode operand sizes.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Missing signed extension - `push`

Description

Missing signed extension of immediate value when pushing -0x1.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-509

Affected instructions:

0x6aff

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  6AFF              push byte -0x1

Input:

binsec disasm -decode 6aff

Observed output:

          ⎧ 0: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := 255₍₃₂₎
push 0xff ⎨ 1: esp := (esp₍₃₂₎ - 4₍₃₂₎)
          ⎩ 2: goto ({0x00000002; 32}, 0)

Expected output:
Added signed extension.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Missing arithmetic operation - `xadd`

Description

When executing xadd instruction the add operation is forgotten.

Reference:
xadd: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-580

Affected instructions:

0x0fc1c0
0x640fc1c0
0x64670fc1c0
0x670fc1c0

Reproduction guide

Instruction:

00000000  0FC1C0            xadd eax,eax

Input:

pyvex.IRSB("\x0F\xC1\xC0", 0x8048000, archinfo.ArchX86())

Observed output:

IRSB {
   t0:Ity_I32 t1:Ity_I32 t2:Ity_I32 t3:Ity_I32

   00 | ------ IMark(0x0, 3, 0) ------
   01 | t0 = GET:I32(eax)
   02 | PUT(cc_op) = 0x00000003
   03 | PUT(cc_dep1) = t0
   04 | PUT(cc_dep2) = t0
   05 | PUT(cc_ndep) = 0x00000000
   06 | PUT(eax) = t0
   NEXT: PUT(eip) = 0x00000003; Ijk_Boring
}

Expected output:
The add operation is included.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

PyVEX:

#  pip freeze | grep pyvex
pyvex==6.7.4.12

Invalid OF calculation - `sub`

Description

Incorrectly calculates overflow flag OF.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-652

Affected instructions:

0x28c0
0x29c0
0x2ac0
0x2bc0

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  28C0              sub al,al

Input:

bap-mc "28c0" --show-bil --arch=X86

Observed output:

{
  v1 := low:8[low:32[EAX]]
  EAX := (extract: 31:8[EAX]).((low:8[low:32[EAX]]) - (low:8[low:32[EAX]]))
  CF := v1 < (low:8[low:32[EAX]])
  OF := high:1[(v1 ^ (low:8[low:32[EAX]])) & (v1 ^ (low:8[low:32[EAX]]))]
  AF := 0x10:8 = (0x10:8 & (((low:8[low:32[EAX]]) ^ v1) ^ (low:8[low:32[EAX]])))
  PF := ~(low:1[let v2 = ((low:8[low:32[EAX]]) >> 0x4:8) ^ (low:8[low:32[EAX]]) in
    let v2 = (v2 >> 0x2:8) ^ v2 in
    (v2 >> 0x1:8) ^ v2])
  SF := high:1[low:8[low:32[EAX]]]
  ZF := 0x0:8 = (low:8[low:32[EAX]])
}

Expected output:
OF should be cleared whenever the given two operands are identical.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Invalid stack operation - `pop`

Description

When execution pop esp the memory is accessed before incrementing the stack pointer. According to the Intel manual, "The POP ESP instruction increments the stack pointer (ESP) before data at the old top of stack is written into the
destination."

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-384

Affected instructions:

0x5c    # pop

Reproduction guide

Instruction:

00000000  5C                pop esp

Input:

binsec disasm -decode 5c

Observed output:

        ⎧ 0: esp := @[esp₍₃₂₎]₄
pop esp ⎨ 1: esp := (esp₍₃₂₎ + 4₍₃₂₎)
        ⎩ 2: goto ({0x00000001; 32}, 0)

Expected output:

pop esp ⎧ 0: esp := @[esp₍₃₂₎]₄
        ⎩ 1: goto ({0x00000001; 32}, 0)

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Confusion of source and destination operands - `xadd`

Description

Instruction xadd occasionally confuses source and destination operand, by writing to the wrong one. The sum of the operands should be written to the destination operand, i.e. the first one, but instead writes to source operand.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-580

Affected instructions:

0x0fc100    # xadd

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  0FC100            xadd [eax],eax

Input:

bap-mc "0fc100" --show-bil --arch=X86

Observed output:

{
  v1 := (low:32[EAX]) + (mem32[pad:32[low:32[EAX]], el]:u32)
  mem32 := mem32 with [pad:32[low:32[EAX]], el]:u32 <- low:32[EAX]
  EAX := v1
  CF := (low:32[EAX]) < v1
  OF := ((high:1[v1]) = (high:1[mem32[pad:32[low:32[EAX]], el]:u32])) & ((high:1[v1]) ^ (high:1[low:32[EAX]]))
  AF := 0x10:32 = (0x10:32 & (((low:32[EAX]) ^ v1) ^ (mem32[pad:32[low:32[EAX]], el]:u32)))
  PF := ~(low:1[let v2 = ((low:32[EAX]) >> 0x4:32) ^ (low:32[EAX]) in
    let v2 = (v2 >> 0x2:32) ^ v2 in
    (v2 >> 0x1:32) ^ v2])
  SF := high:1[low:32[EAX]]
  ZF := 0x0:32 = (low:32[EAX])
}

Expected output:
Instead of writing v1 to EAX, it should be written to the memory of EAX.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Not taking part of value - `bt`, `bts`, `sbb`

Description

During some shift instructions, the shift offset operand is not decoded properly. The lowest five bits should be taken and not the whole operand. Currently the bit base is shifted out of the resulting value.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-113
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-119
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-587

Affected instructions:

0x0fa300    # bt
0x0fab00    # bts
0xf21900    # sbb
0xf21b00

Reproduction guide

Instruction:

00000000  0FA300            bt [eax],eax

Input:

binsec disasm -decode 0fa300

Observed output:

              ⎧ 0: CF := (@[eax₍₃₂₎]₄ ≫𝒖 eax₍₃₂₎){0}
              ⎪ 1: OF := \undef
              ⎪ 2: SF := \undef
bt [eax], eax ⎨ 3: AF := \undef
              ⎪ 4: PF := \undef
              ⎩ 5: goto ({0x00000003; 32}, 0)

Expected output:
Take only the lowest five bits from the offset operand.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Operand address changed - `xchg`, `xadd`, `cmpsb`, `cmpsd`

Description

The address of the destination operand is changed before being written to. In some cases directly and obvious, other cases where the calculation of EFLAGS uses an address already changed where the old value should have been used.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-585
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-580
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-169

Affected instructions:

0x8600     # xchg
0x0fc000   # xadd
0x0fc100
0xa6       # cmpsb
0xa7       # cmpsd

Reproduction guide

Instruction:

00000000  8600              xchg al,[eax]

Input:

binsec disasm -decode 8600

Observed output:

      ⎧ 0: temp8 := eax₍₃₂₎{0,7}
      ⎪ 1: eax{0, 7} := @[eax₍₃₂₎]₁
xchg8 ⎨ 2: @[eax₍₃₂₎]₁ := temp8₍₈₎
      ⎩ 3: goto ({0x00000002; 32}, 0)

Expected output:
Not manipulate destination address before write.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Operand address changed - `sub`

Description

Destination address, specified in the first operand, is changed before being written to.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-652

Affected instructions:

0x2a00
0x2b00

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  2A00              sub al,[eax]

Input:

bap-mc "2a00" --show-bil --arch=X86

Observed output:

{
  v1 := low:8[low:32[EAX]]
  EAX := (extract: 31:8[EAX]).((low:8[low:32[EAX]]) - (mem32[pad:32[low:32[EAX]], el]:u8))
  CF := v1 < (mem32[pad:32[low:32[EAX]], el]:u8)
  OF := high:1[(v1 ^ (mem32[pad:32[low:32[EAX]], el]:u8)) & (v1 ^ (low:8[low:32[EAX]]))]
  AF := 0x10:8 = (0x10:8 & (((low:8[low:32[EAX]]) ^ v1) ^ (mem32[pad:32[low:32[EAX]], el]:u8)))
  PF := ~(low:1[let v2 = ((low:8[low:32[EAX]]) >> 0x4:8) ^ (low:8[low:32[EAX]]) in
    let v2 = (v2 >> 0x2:8) ^ v2 in
    (v2 >> 0x1:8) ^ v2])
  SF := high:1[low:8[low:32[EAX]]]
  ZF := 0x0:8 = (low:8[low:32[EAX]])
}

Expected output:
Not to change address in destination operand before write.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Webpage improvement

Please fix the following issues before the ASE deadline.

Describe what the project is about. People should be able to know what the web page is about when they first visit the page.
The page currently has several tables, but it is not clear whether the table is about bugs found.
Clearly show the versions of each lifters we tested.
Have a link to our paper PDF and the source code.

Invalid AF calculation - `scasb`, `scasd`, `add`, `adc`, `sbb`, `sub`, `cmp`, `inc`, `dec`

Description

The AF flag is being calculated in much the same way as the OF flag, but this is not the correct behaviour. Instead of taking the carry of a whole byte, it should take the 5th bit (zero indexed), as a decimal number is represented by five bits in BCD.

Reference:
scasb, scasd: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-590
adc: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-26
add: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-31
sbb: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-587
sub: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-652
cmp: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-153
inc: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-451
dec: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-285

Affected instructions:

0xae         # scasb
0xaf         # scasd
0x0000       # add
0x0100
0x0200
0x0300
0x0442
0x0542424242
0x1000       # adc
0x1100
0x1200
0x1300
0x1400
0x1500000000
0x18c0       # sbb
0x19c0
0x1ac0
0x1bc0
0x1c00
0x1d00000000
0x2800       # sub
0x2900
0x2a08
0x2b08
0x2c42
0x3800       # cmp
0x3900
0x3a00
0x3b00
0x3c42
0x3d42424242
0x40         # inc
0x41
0x42
0x43
0x44
0x45
0x46
0x47
0xfe00
0xff00
0x48         # dec
0x49
0x4a
0x4b
0x4c
0x4d
0x4e
0x4f

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  0000              add [eax],al

Input:

binsec disasm -decode 0000

Observed output:

              ⎧ 0: res8 := (@[eax₍₃₂₎]₁ + eax₍₃₂₎{0,7})
              ⎪ 1: OF := ((@[eax₍₃₂₎]₁{7} = eax₍₃₂₎{0,7}{7}) && (@[eax₍₃₂₎]₁{7} ≠ res8₍₈₎{7}))
              ⎪ 2: SF := (res8₍₈₎ <𝒔 0₍₈₎)
              ⎪ 3: ZF := (res8₍₈₎ = 0₍₈₎)
add [eax], al ⎨ 4: AF := ((extu @[eax₍₃₂₎]₁{0,7} 9) + (extu eax₍₃₂₎{0,7}{0,7} 9)){8}
              ⎪ 5: PF := ¬(((((((res8₍₈₎{0} ⨁ res8₍₈₎{1}) ⨁ res8₍₈₎{2}) ⨁ res8₍₈₎{3}) ⨁ res8₍₈₎{4}) ⨁ res8₍₈₎{5}) ⨁ res8₍₈₎{6}) ⨁ res8₍₈₎{7})
              ⎪ 6: CF := ((extu @[eax₍₃₂₎]₁ 9) + (extu eax₍₃₂₎{0,7} 9)){8}
              ⎪ 7: @[eax₍₃₂₎]₁ := res8₍₈₎
              ⎩ 8: goto ({0x00000002; 32}, 0)

Expected output:
Something like this BAP code:

  v1 := mem32[pad:32[low:32[EAX]], el]:u8
  v2 := low:8[low:32[EAX]]
  AF := 0x10:8 = (0x10:8 & (((mem32[pad:32[low:32[EAX]], el]:u8) ^ v1) ^ v2))

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Useless memory access - `bt`, `bts`, `btr`, `btc`

Description

Using some seemingly useless memory for simple register operation with operands 0x0c and 0xc8.

CF <- Bit(Bitcase, BitOffset)

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-113

Affected instructions:

0x0fa3c0    # bt
0x0fa3c8
0x0fabc0    # bts
0x0fabc8
0x0fb3c0    # btr
0x0fb3c8
0x0fbbc0    # btc
0x0fbbc8

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  0FA3C0            bt eax,eax

Input:

pyvex.IRSB("\x0F\xA3\xC0", 0x8048000, archinfo.ArchX86())

Observed output:

IRSB {
   t0:Ity_I8 t1:Ity_I8 t2:Ity_I32 t3:Ity_I32 t4:Ity_I8 t5:Ity_I32 t6:Ity_I32 t7:Ity_I32 t8:Ity_I32 t9:Ity_I32 t10:Ity_I32 t11:Ity_I32 t12:Ity_I32 t13:Ity_I8 t14:Ity_I32 t15:Ity_I32 t16:Ity_I32 t17:Ity_I32 t18:Ity_I32 t19:Ity_I32 t20:Ity_I32

   00 | ------ IMark(0x0, 3, 0) ------
   01 | t2 = GET:I32(eax)
   02 | t9 = GET:I32(esp)
   03 | t8 = Sub32(t9,0x00000080)
   04 | PUT(esp) = t8
   05 | STle(t8) = t2
   06 | t3 = And32(t2,0x0000001f)
   07 | t12 = Sar32(t3,0x03)
   08 | t11 = Add32(t8,t12)
   09 | t14 = And32(t3,0x00000007)
   10 | t13 = 32to8(t14)
   11 | t0 = LDle:I8(t11)
   12 | PUT(cc_op) = 0x00000000
   13 | PUT(cc_dep2) = 0x00000000
   14 | t17 = 8Uto32(t0)
   15 | t16 = Shr32(t17,t13)
   16 | t15 = And32(t16,0x00000001)
   17 | PUT(cc_dep1) = t15
   18 | PUT(cc_ndep) = 0x00000000
   19 | t18 = LDle:I32(t8)
   20 | PUT(eax) = t18
   21 | t19 = Add32(t8,0x00000080)
   22 | PUT(esp) = t19
   NEXT: PUT(eip) = 0x00000003; Ijk_Boring
}

Expected output:
Not using useless memory.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

PyVEX:

#  pip freeze | grep pyvex
pyvex==6.7.4.12

Confusion of source and destination operands - `palingr`, `cmpxchg`

Description

Some instructions occasionally confuses source and destination operand, by writing to the wrong one. The sum of the operands should be written to the destination operand, i.e. the first one, but instead writes to source operand.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-219
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-181

Affected instructions:

0x0f3a0f0042    # palingr
0x64660fb100    # cmpxchg

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  0F3A0F0042        palignr mm0,[eax],0x42

Input:

binsec disasm -decode 0f3a0f0042

Observed output:

            ⎧ 0: temp128 := (xmm0₍₁₂₈₎{0,63} :: @[eax₍₃₂₎]₈)
            ⎪ 1: temp128 := (temp128₍₁₂₈₎ ≫𝒖 528₍₃₂₎)
            ⎪ 2: temp64 := @[eax₍₃₂₎]₈
palignr ... ⎨ 3: temp64{0, 63} := temp128₍₁₂₈₎{0,63}
            ⎪ 4: @[eax₍₃₂₎]₈ := temp64₍₆₄₎
            ⎩ 5: goto ({0x00000005; 32}, 0)

Expected output:
Instead of writing to EAX, it should be written to mm0.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Not storing segment register - `mov` [x64]

Description

When attempting to move a segment register, for instance ES into a 64-bit register using a REX prefix, the segment register is ignored.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-35

Affected instructions:

0x488c00

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  488C00            mov qword [rax],es

Input:

pyvex.IRSB("\x48\x8C\x00", 0x8048000, archinfo.ArchX86())

Observed output:

IRSB {
   t0:Ity_I64 t1:Ity_I64

   00 | ------ IMark(0x0, 3, 0) ------
   01 | t0 = GET:I64(rax)
   02 | STle(t0) = 0x0000
   NEXT: PUT(rip) = 0x0000000000000003; Ijk_Boring
}

Expected output:

IRSB {
   t0:Ity_I64 t1:Ity_I16

   00 | ------ IMark(0x0, 3, 0) ------
   01 | t0 = GET:I64(rax)
   01 | t1 = GET:I16(es)
   02 | STle(t0) = t1
   NEXT: PUT(rip) = 0x0000000000000003; Ijk_Boring
}

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

PyVEX:

#  pip freeze | grep pyvex
pyvex==6.7.4.12

Invalid pushad behaviour - `pushad`

Description

When executing pushad, the value of EBX is pushed and immediately overwritten by the original value of ESP. In result only 7 registers of the expected 8, EAX, ECX, EDX, EBX, original ESP, EBP,ESI, and EDI, are pushed.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-512

Affected instructions:

0x60
0x6460
0x6760

Reproduction guide

Instruction:

00000000  60                pushad

Input:

binsec disasm -decode 60

Observed output:

       ⎧ 0: temp32 := esp₍₃₂₎
       ⎪ 1: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 2: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := eax₍₃₂₎
       ⎪ 3: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 4: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ecx₍₃₂₎
       ⎪ 5: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 6: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := edx₍₃₂₎
       ⎪ 7: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 8: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ebx₍₃₂₎
pushal ⎨ 9: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := temp32₍₃₂₎
       ⎪10: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪11: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪12: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ebp₍₃₂₎
       ⎪13: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪14: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := esi₍₃₂₎
       ⎪15: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪16: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := edi₍₃₂₎
       ⎩17: goto ({0x00000001; 32}, 0)

Expected output:
Correctly push all 8 general purpose registers to the stack.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Maintenance Issue

I'm trying to build this project so I can get insight about when multiple IRs translated into one common IR (UIR).
But all the trials to build MeanDiff failed including;

The method described in Readmd.md
Building this repo on the Ubuntu 16.10 VM
Troubleshooting by modifing the Dockerfile in this repo

I checked last commit of this repo was on 2017.
I'm curious about whether additional maintenance to this repo(+Readmd.md) will be done so that other people (including me) can successfully build MeanDiff.

No memory alignment - `movaps`, `movdqa`

Description

The instructions movaps and movdqa does not enforce the required 16-byte alignment. According to the Intel manual, "When the source or destination operand is a memory operand, the operand must be aligned on a 16[...]-byte boundary or a general-protection exception (#GP) will be generated."

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-49
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-62

Affected instructions:

0x0f28042542424242     # movaps
0x0f280425ffffffff
0x0f29042542424242
0x0f290425ffffffff

0x660f6f042542424242   # movdqa
0x660f6f0425ffffffff
0x660f7f042542424242
0x660f7f0425ffffffff

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  0F28042542424242  movaps xmm0,oword [0x42424242]

Input:

binsec disasm -decode 0f28042542424242

Observed output:

mov xmm0, [0x42424242] ⎧1: xmm0 := @[1111638594₍₃₂₎]₁₆
                       ⎩2: goto ({0x00000008; 32}, 0)

Expected output:
Enforce the memory alignment by exiting with some error.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

No memory alignment - `pshufb`

Description

Missing enforcement of memory alignment of pshufb with certain values of source operand. Operand should be 16-byte boundary aligned when 128-bit memory.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-410

Affected instructions:

0x660f3800042542424242
0x660f38000425ffffffff
0x660f38000542424242
0x660f380005ffffffff
0x660f38000d42424242
0x660f38000dffffffff

Reproduction guide

Instruction:

00000000  660F380004254242  pshufb xmm0,[0x42424242] -4242

Input:

bap-mc "660f3800042542424242" --show-bil --arch=X86

Observed output:

  YMM0 := (extract: 255:128[YMM0]).((((((((((((((((if extract: 127:127[mem32[0x42424242:32, el]:u128]
                                                     then 0x0:8
                                                     else low:8[(low:128[YMM0]) >> ((pad:128[extract: 123:120[mem32[0x42424242:32, el]:u128]]) * 0x8:128)]).(
    if extract: 119:119[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 115:112[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 111:111[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 107:104[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 103:103[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 99:96[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 95:95[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 91:88[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 87:87[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 83:80[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 79:79[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 75:72[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 71:71[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 67:64[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 63:63[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 59:56[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 55:55[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 51:48[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 47:47[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 43:40[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 39:39[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 35:32[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 31:31[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 27:24[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 23:23[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 19:16[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 15:15[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 11:8[mem32[0x42424242:32, el]:u128]]) * 0x8:128)])).(
    if extract: 7:7[mem32[0x42424242:32, el]:u128] then 0x0:8
      else low:8[(low:128[YMM0]) >> ((pad:128[extract: 3:0[mem32[0x42424242:32, el]:u128]]) * 0x8:128)]))
}

Expected output:
Something like:

{
  YMM0 := (extract: 255:128[YMM0]).(pad:128[mem32[0x42424242:32, el]:u128])
  if ((0x42424242:32 & 0xF:32) = 0x0:32) {
    
  }
  else {
    cpuexn (13)
  }
}

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Invalid CF calculation - `xadd`

Description

Invalid calculation of the carry flag, CF, when executing xadd instruction with the 0xc0 as operand and prefixed as below.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 5-580 Vol. 2C

Affected instructions:

0xc1
0x64660fc1c0
0x6466670fc1c0
0x660fc1c0
0x66670fc1c0
0xf20fc1c0
0xf2640fc1c0
0xf264660fc1c0
0xf26466670fc1c0
0xf264670fc1c0
0xf2660fc1c0
0xf266670fc1c0
0xf2670fc1c0
0xf30fc1c0
0xf3640fc1c0
0xf364660fc1c0
0xf36466670fc1c0
0xf364670fc1c0
0xf3660fc1c0
0xf366670fc1c0
0xf3670fc1c0

Reproduction guide

Instruction:

00000000  64660FC1C0        fs xadd ax,ax

Input:

bap-mc "64660fc1c0" --show-bil --arch=X86

Observed output:

{
  v1 := (low:16[low:32[EAX]]) + (low:16[low:32[EAX]])
  EAX := (extract: 31:16[EAX]).(low:16[low:32[EAX]])
  EAX := (extract: 31:16[EAX]).v1
  CF := (low:16[low:32[EAX]]) < v1
  OF := ((high:1[v1]) = (high:1[low:16[low:32[EAX]]])) & ((high:1[v1]) ^ (high:1[low:16[low:32[EAX]]]))
  AF := 0x10:16 = (0x10:16 & (((low:16[low:32[EAX]]) ^ v1) ^ (low:16[low:32[EAX]])))
  PF := ~(low:1[let v2 = ((low:16[low:32[EAX]]) >> 0x4:16) ^ (low:16[low:32[EAX]]) in
    let v2 = (v2 >> 0x2:16) ^ v2 in
    (v2 >> 0x1:16) ^ v2])
  SF := high:1[low:16[low:32[EAX]]]
  ZF := 0x0:16 = (low:16[low:32[EAX]])
}

Expected output:
With this implementation, CF is only set to zero.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Invalid OF calculation - `xadd`, `sbb`

Description

Invalid calculation of the carry flag, OF, when executing xadd instruction.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-580

Affected instructions:

0x0fc1c0   # xadd
0x1800     # sbb
0x1a00

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  1800              sbb [eax],al

Input:

binsec disasm -decode 1800

Observed output:

              ⎧ 0: res8 := (@[eax₍₃₂₎]₁ - (eax₍₃₂₎{0,7} + (extu CF₍₁₎ 8)))
              ⎪ 1: OF := ((@[eax₍₃₂₎]₁{7} ≠ (@[eax₍₃₂₎]₁ + (extu CF₍₁₎ 8)){7}) && (@[eax₍₃₂₎]₁{7} ≠ res8₍₈₎{7}))
              ⎪ 2: SF := (res8₍₈₎ <𝒔 0₍₈₎)
              ⎪ 3: ZF := (res8₍₈₎ = 0₍₈₎)
sbb [eax], al ⎨ 4: AF := (@[eax₍₃₂₎]₁{0,7} <𝒖 (eax₍₃₂₎{0,7}{0,7} + (extu AF₍₁₎ 8)))
              ⎪ 5: PF := ¬(((((((res8₍₈₎{0} ⨁ res8₍₈₎{1}) ⨁ res8₍₈₎{2}) ⨁ res8₍₈₎{3}) ⨁ res8₍₈₎{4}) ⨁ res8₍₈₎{5}) ⨁ res8₍₈₎{6}) ⨁ res8₍₈₎{7})
              ⎪ 6: CF := (@[eax₍₃₂₎]₁ <𝒖 (eax₍₃₂₎{0,7} + (extu CF₍₁₎ 8)))
              ⎪ 7: @[eax₍₃₂₎]₁ := res8₍₈₎
              ⎩ 8: goto ({0x00000002; 32}, 0)

Expected output:
The RHS of first clause of OF should be (eax₍₃₂₎{0,7} + (extu CF₍₁₎ 8)){7}.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Invalid order of calculation - `cmpxchg`

Description

When executing cmpxchg, the semantics for comparison is accumulator minus destination operand, but they are switched.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-181

Affected instructions:

0x0fb100    #cmpxchg

Reproduction guide

Instruction:

00000000  0FB100            cmpxchg [eax],eax

Input:

binsec disasm -decode 0fb100

Observed output:

                   ⎧ 0: res32 := (@[eax₍₃₂₎]₄ - eax₍₃₂₎)
                   ⎪ 1: OF := ((@[eax₍₃₂₎]₄{31} ≠ eax₍₃₂₎{31}) && (@[eax₍₃₂₎]₄{31} ≠ res32₍₃₂₎{31}))
                   ⎪ 2: SF := (res32₍₃₂₎ <𝒔 0₍₃₂₎)
                   ⎪ 3: ZF := (res32₍₃₂₎ = 0₍₃₂₎)
                   ⎪ 4: AF := (@[eax₍₃₂₎]₄{0,7} <𝒖 eax₍₃₂₎{0,7})
                   ⎪ 5: PF := ¬(((((((res32₍₃₂₎{0} ⨁ res32₍₃₂₎{1}) ⨁ res32₍₃₂₎{2}) ⨁ res32₍₃₂₎{3}) ⨁ res32₍₃₂₎{4}) ⨁ res32₍₃₂₎{5}) ⨁ res32₍₃₂₎{6}) ⨁ res32₍₃₂₎{7})
cmpxchg [eax], eax ⎨ 6: CF := (@[eax₍₃₂₎]₄ <𝒖 eax₍₃₂₎)
                   ⎪ 7: if (eax₍₃₂₎ = @[eax₍₃₂₎]₄) goto 10 else goto 8
                   ⎪ 8: eax := @[eax₍₃₂₎]₄
                   ⎪ 9: goto 11 
                   ⎪10: @[eax₍₃₂₎]₄ := eax₍₃₂₎
                   ⎩11: goto ({0x00000003; 32}, 0)

Expected output:
Correct order of operands during calculation.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Invalid store/load AF behaviour - `sahf`, `lahf`

Description

When executing the sahf or lahff instructions, AH should be stored or loaded, but rather AL is used.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-578
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-517

Affected instructions:

0x9e    # sahf
0x9f    # lahf

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  9E                sahf

Input:

binsec disasm -decode 9e

Observed output:

     ⎧ 0: SF := eax₍₃₂₎{7}
     ⎪ 1: ZF := eax₍₃₂₎{6}
     ⎪ 2: AF := eax₍₃₂₎{4}
sahf ⎨ 3: PF := eax₍₃₂₎{2}
     ⎪ 4: CF := eax₍₃₂₎{0}
     ⎩ 5: goto ({0x00000001; 32}, 0)

Expected output:
Use AH instead of AL.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1

Not taking mod size - `rol`, `ror`

Description

When executing instructions rol and ror, the count is sometimes calculated without taking the correct mod size, where size is the operand size.

According to manual, the correct semantics for calculating count:
tempCOUNT ← (COUNT & COUNTMASK) MOD SIZE

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-519

Affected instructions:

0xc000ff     # rol
0xd200
0x66c100ff
0xd208       # ror
0x66d200
0x66d300

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  C000FF            rol byte [eax],byte 0xff

Input:

bap-mc "c000ff" --show-bil --arch=X86

Observed output:

{
  orig_count1 := 0xFF:8 & 0x1F:8
  mem32 := mem32
             with [pad:32[low:32[EAX]], el]:u8 <- ((mem32[pad:32[low:32[EAX]], el]:u8) << orig_count1) | ((mem32[pad:32[low:32[EAX]], el]:u8) >> (0x8:8 - orig_count1))
  CF := if orig_count1 = 0x0:8 then CF
          else low:1[mem32[pad:32[low:32[EAX]], el]:u8]
  OF := if orig_count1 = 0x0:8 then OF
          else if orig_count1 = 0x1:8
                 then CF ^ (high:1[mem32[pad:32[low:32[EAX]], el]:u8])
                 else unknown[OF undefined after rotate of more then 1 bit]:u1
}

Expected output:
orig_count1 is calculated with taking mod of operator size (8).

Rappel

A more specific example done in Rappel using the same instruction as above, with [EAX] set to 0xfd.

~/repos/rappel/bin(master) » ./rappel
eax: 0x00000000 ebx: 0x00000000 ecx: 0x00000000 edx: 0x00000000
esi: 0x00000000 edi: 0x00000000
eip: 0x00400001 esp: 0xffe64510 ebp: 0x00000000
flags: 0x00000202 [cf:0, zf:0, of:0, sf:0, pf:0, af:0, df:0]
> mov byte [esp], 0xfd
eax: 0x00000000 ebx: 0x00000000 ecx: 0x00000000 edx: 0x00000000
esi: 0x00000000 edi: 0x00000000
eip: 0x00400005 esp: 0xffe64510 ebp: 0x00000000
flags: 0x00000202 [cf:0, zf:0, of:0, sf:0, pf:0, af:0, df:0]
> mov eax, esp
eax: 0xffe64510 ebx: 0x00000000 ecx: 0x00000000 edx: 0x00000000
esi: 0x00000000 edi: 0x00000000
eip: 0x00400003 esp: 0xffe64510 ebp: 0x00000000
flags: 0x00000202 [cf:0, zf:0, of:0, sf:0, pf:0, af:0, df:0]
> rol byte [eax], byte 0xff
eax: 0xffe64510 ebx: 0x00000000 ecx: 0x00000000 edx: 0x00000000
esi: 0x00000000 edi: 0x00000000
eip: 0x00400004 esp: 0xffe64510 ebp: 0x00000000
flags: 0x00000202 [cf:0, zf:0, of:0, sf:0, pf:0, af:0, df:0]
> mov ebx, [esp]
eax: 0xffe64510 ebx: 0x000000fe ecx: 0x00000000 edx: 0x00000000
esi: 0x00000000 edi: 0x00000000
eip: 0x00400004 esp: 0xffe64510 ebp: 0x00000000
flags: 0x00000202 [cf:0, zf:0, of:0, sf:0, pf:0, af:0, df:0]
>

According to manual, the correct calculation of tempCount should be ((0xff & 0x1f) % 8), which equals 7.

In the BIL output showed above, count is calculated to 0xff & 0x1f, which is incorrect.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

Missing signed extension - `push`

Description

Missing signed extension of immediate value when pushing -0x1.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-509

Affected instructions:

0x6aff

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  6AFF              push byte -0x1

Input:

bap-mc "6aff" --show-bil --arch=X86

Observed output:

{
  v1 := 0xFF:32
  ESP := ESP - 0x4:32
  mem32 := mem32 with [ESP, el]:u32 <- v1
}

Expected output:
Added signed extension.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0

TODOs before the final release

The README.md should be updated in the master branch.
There should be a build script that builds all the code.

Example code for testing ARM lifting

Hi,

I would like to test ARM lifting for BAP and pyVEX, but I am puzzled by the CLI interface.
How does one go about generating instructions to test and to feed to the lifters?
The usage part in the README is still to be done.

Could you please provide a minimum working example for testing instructions other than x86/x64?

Thank you.

Invalid stack operation - `push`, `pop`

Description

When pushing segment registers, as SS, CS, DS, ES, FS and GS, the stack pointer is incremented by four bytes, although the segment registers are only two bytes of size. According to the Intel manual, "The operand size (16, 32, or 64 bits) determines the amount by which the stack pointer is decremented (2, 4 or 8)."

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-509

Affected instructions:

0x06    # push
0x0e
0x0fa0
0x0fa8
0x16
0x1e
0x07    # pop
0x0fa1
0x0fa9
0x17
0x1f

Reproduction guide

Instruction:

00000000  06                push es

Input:

pyvex.IRSB("\x06", 0x8048000, archinfo.ArchX86())

Observed output:

IRSB {
   t0:Ity_I16 t1:Ity_I32 t2:Ity_I32 t3:Ity_I32 t4:Ity_I32

   00 | ------ IMark(0x0, 1, 0) ------
   01 | t0 = GET:I16(es)
   02 | t3 = GET:I32(esp)
   03 | t2 = Sub32(t3,0x00000004)
   04 | PUT(esp) = t2
   05 | STle(t2) = t0
   NEXT: PUT(eip) = 0x00000001; Ijk_Boring
}

Expected output:
Subtract only two bytes from ESP:

IRSB {
   t0:Ity_I16 t1:Ity_I32 t2:Ity_I32 t3:Ity_I32 t4:Ity_I32

   00 | ------ IMark(0x0, 1, 0) ------
   01 | t0 = GET:I16(es)
   02 | t3 = GET:I32(esp)
   03 | t2 = Sub32(t3,0x00000002)    <-----
   04 | PUT(esp) = t2
   05 | STle(t2) = t0
   NEXT: PUT(eip) = 0x00000001; Ijk_Boring
}

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

PyVEX:

#  pip freeze | grep pyvex
pyvex==6.7.4.12

Invalid CF calculation - `sbb`

Description

Invalid calculation of the carry flag, CF, when executing sbb instructions with the opcodes below.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-587

Affected instructions:

0x1900    # sbb
0x1B00
0x1CFF

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  1900              sbb [eax],eax

Input:

binsec disasm -decode 1900

Observed output:

               ⎧ 0: res32 := (@[eax₍₃₂₎]₄ - (eax₍₃₂₎ + (extu CF₍₁₎ 32)))
               ⎪ 1: OF := ((@[eax₍₃₂₎]₄{31} ≠ (@[eax₍₃₂₎]₄ + (extu CF₍₁₎ 32)){31}) && (@[eax₍₃₂₎]₄{31} ≠ res32₍₃₂₎{31}))
               ⎪ 2: SF := (res32₍₃₂₎ <𝒔 0₍₃₂₎)
               ⎪ 3: ZF := (res32₍₃₂₎ = 0₍₃₂₎)
sbb [eax], eax ⎨ 4: AF := (@[eax₍₃₂₎]₄{0,7} <𝒖 (eax₍₃₂₎{0,7} + (extu AF₍₁₎ 8)))
               ⎪ 5: PF := ¬(((((((res32₍₃₂₎{0} ⨁ res32₍₃₂₎{1}) ⨁ res32₍₃₂₎{2}) ⨁ res32₍₃₂₎{3}) ⨁ res32₍₃₂₎{4}) ⨁ res32₍₃₂₎{5}) ⨁ res32₍₃₂₎{6}) ⨁ res32₍₃₂₎{7})
               ⎪ 6: CF := (@[eax₍₃₂₎]₄ <𝒖 (eax₍₃₂₎ + (extu CF₍₁₎ 32)))
               ⎪ 7: @[eax₍₃₂₎]₄ := res32₍₃₂₎
               ⎩ 8: goto ({0x00000002; 32}, 0)

Expected output:
It cannot detect the overflow situation correctly when the destination operand is negative.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1