Hi Dan,
On Thu, Apr 19, 2018 at 08:15:10AM +0300, Dan Carpenter wrote:
> Several people have asked me to write this and I think one person was
> maybe working on writing it themselves...
>
> The point of this check is to find place which might be vulnerable to
> the Spectre vulnerability. In the kernel we have the array_index_nospec()
> macro which turns off speculation. There are fewer than 10 places where
> it's used. Meanwhile this check complains about 800 places where maybe
> it could be used. Probably the 100x difference means there is something
> that I haven't understood...
>
> What the test does is it looks at array accesses where the user controls
> the offset. It asks "is this a read?" and have we used the
> array_index_nospec() macro? If the answers are yes, and no respectively
> then print a warning.
>
> http://repo.or.cz/smatch.git/blob/HEAD:/check_spectre.c
>
> The other thing is that speculation probably goes to 200 instructions
> ahead at most. But the Smatch doesn't have any concept of CPU
> instructions. I've marked the offsets which were recently compared to
> something as "local cap" because they were probably compared to the
> array limit. Those are maybe more likely to be under the 200 CPU
> instruction count.
>
> This obviously a first draft.
>
> What would help me, is maybe people could tell me why there are so many
> false positives. Saying "the lower level checks for that" is not
> helpful but if you could tell me the exact function name where the check
> is that helps a lot...
Running this over an arm64 v4.17-rc2, I thought I'd found a
false-positive, but I've now convinced myself that we have a class of
false-negatives.
The short story is:
1) Compiler transformations mean that under speculation, a variable can
behave as-if it is a larger type, e.g. an unsigned char can hold any
value in the range 0..~0ULL. This full range can be used when
performing an array access.
This means that implicit narrowing cannot be relied upon under
speculation; any variable may behave as-if it is an unsigned long
long.
2) Compiler transformations can elide binary operations, so we cannot
rely on source level AND (&) or MOD (%) operations to narrow the
range of an expression, regardless of the types of either operand.
This means that source-level AND and MOD operations cannot be relied
upon under speculation.
3) MOD (%) operations may be implemented with branchy library code. Even
where the compiler cannot elide a MOD, it can be effectively skipped
under speculation.
This means that source-level MOD operations cannot be relied upon
under speculation, *even if we can make the inputs and outputs opaque
to the compiler*.
I think this means that *any* expression, regardless of its type must be
considered as having the full range of the machine's word size, unless a
compiler-opaque bounding operation like array_index_nospec() has been
used to sanitize that expression.
For smatch, this means that the result of check_spectre.c's
get_may_by_type() may be misleading, and we may be throwing away valid
spectre gadgets.
I suspect this means *many* more potential spectre gadgets. :(
More details/examples below.
1: larger types under speculation
-----------------------------------------------------------------------
I don't believe that we can assume that (under speculation) sub-word
types are actually bounded by their type's size. The compiler can elide
narrowing where it (validly) believes a value is sufficiently small,
e.g. for code like:
int array[256];
static int foo(unsigned char idx)
{
return array[idx];
}
int bar(unsigned long idx)
{
if (idx < 256)
return foo(idx);
return 0;
}
... GCC will generate the following at -O2:
x86-64
----
0000000000000000 <bar>:
0: 31 c0 xor %eax,%eax
2: 48 81 ff ff 00 00 00 cmp $0xff,%rdi
9: 77 0d ja 18 <bar+0x18>
b: 48 8d 05 00 00 00 00 lea 0x0(%rip),%rax # 12 <bar+0x12>
12: 48 63 ff movslq %edi,%rdi
15: 8b 04 b8 mov (%rax,%rdi,4),%eax
18: f3 c3 repz retq
arm64
-----
0000000000000000 <bar>:
0: f103fc1f cmp x0, #0xff
4: 540000a8 b.hi 18 <bar+0x18> // b.pmore
8: 90000001 adrp x1, 400 <bar+0x400>
c: 91000021 add x1, x1, #0x0
10: b860d820 ldr w0, [x1, w0, sxtw #2]
14: d65f03c0 ret
18: 52800000 mov w0, #0x0 // #0
1c: d65f03c0 ret
After the test, GCC trusts that bits 31:8 of idx must be zero, though
for some reason doesn't trust bits 63:32, which seems like a missed
optimization given it requires a pointless movslq on x86-64.
Then GCC performs the array access with bits 31:0 of idx, so if the
bounds check we mis-predicted, we can access array[0x0...0xffffffff]
rather than array[0x0...0xff] as might be expected from the type of the
expression using idx to access the array in foo.
2: elision of binary operations (and associated narrowing)
-----------------------------------------------------------------------
Explicit AND binops can be elided:
int some_array[256];
static int foo(unsigned long a)
{
unsigned char mask = 0xff;
return some_array[a & mask];
}
int bar(unsigned long a)
{
if (a < 256)
return foo(a);
return 0;
}
... where GCC -O2 gives us:
x86-64
------
0000000000000000 <bar>:
0: 31 c0 xor %eax,%eax
2: 48 81 ff ff 00 00 00 cmp $0xff,%rdi
9: 77 0a ja 15 <bar+0x15>
b: 48 8d 05 00 00 00 00 lea 0x0(%rip),%rax # 12 <bar+0x12>
12: 8b 04 b8 mov (%rax,%rdi,4),%eax
15: f3 c3 repz retq
arm64
-----
0000000000000000 <bar>:
0: f103fc1f cmp x0, #0xff
4: 540000a8 b.hi 18 <bar+0x18> // b.pmore
8: 90000001 adrp x1, 400 <bar+0x400>
c: 91000021 add x1, x1, #0x0
10: b8607820 ldr w0, [x1, x0, lsl #2]
14: d65f03c0 ret
18: 52800000 mov w0, #0x0 // #0
1c: d65f03c0 ret
... allowing access to array[0x0...0xffffffffffffffff] under
speculation, rather than array[0x0...0xff].
The same applies for MOD operations:
int some_array[256];
static int foo(unsigned long a)
{
unsigned short mod = 256;
a %= mod;
return some_array[a];
}
int bar(unsigned long a)
{
if (a < 256)
return foo(a);
return 0;
}
... where GCC -O2 gives us:
x86-64
------
0000000000000000 <bar>:
0: 31 c0 xor %eax,%eax
2: 48 81 ff ff 00 00 00 cmp $0xff,%rdi
9: 77 0a ja 15 <bar+0x15>
b: 48 8d 05 00 00 00 00 lea 0x0(%rip),%rax # 12 <bar+0x12>
12: 8b 04 b8 mov (%rax,%rdi,4),%eax
15: f3 c3 repz retq
arm64
-----
0000000000000000 <bar>:
0: f103fc1f cmp x0, #0xff
4: 540000a8 b.hi 18 <bar+0x18> // b.pmore
8: 90000001 adrp x1, 400 <bar+0x400>
c: 91000021 add x1, x1, #0x0
10: b8607820 ldr w0, [x1, x0, lsl #2]
14: d65f03c0 ret
18: 52800000 mov w0, #0x0 // #0
1c: d65f03c0 ret
... allowing access to array[0x0...0xffffffffffffffff] under
speculation, rather than array[0x0...0xffff] given that mod was 16-bit.
3: branchy MOD operations
-----------------------------------------------------------------------
On some machines, MOD might be a call to a (branchy) library function
(e.g. __aeabi_uidivmod on ARMv7 without sdiv), and iterative division
could terminate prematurely under speculation, leaving a remainder
larger than the RHS in a register.
e.g. for code like:
extern int array[256];
int bounded_access(unsigned int idx, char bound)
{
idx %= bound;
return array[idx];
}
... GCC can generate the following at -O2:
arm
---
00000000 <bounded_access>:
0: b510 push {r4, lr}
2: f240 0400 movw r4, #0
6: f2c0 0400 movt r4, #0
a: f7ff fffe bl 0 <__aeabi_uidivmod>
e: f854 0021 ldr.w r0, [r4, r1, lsl #2]
12: bd10 pop {r4, pc}
... where under speculation __aeabi_uidivmod could return early, leaving
the remainder in r1 bigger than a char. Thus allowing access to
array[0x0...0xffffffff] under speculation rather than array[0x0..0xff].
Thanks,
Mark.
