[Dailydave] ILLITHID, Darpa, Classes

[Dave Aitel]

So at "Pentacon", which was the DARPA CTF show and tell, I got to spend
five hours explaining what ILLITHID was to DoD executives (NSA people,
Air Force people, etc.). The project next to ours was about using the
TPM to do remote attestation. Basically, it was impossible and would
never work like so many of the "BIOS verification" things on display. I
think if there's one thing that needs to get drilled into people's heads
it's that without full Palladium, you don't get remote attestation. Ask
people this: Can you install a GPG program that can create a key, and
send a signed and encrypted email to a remote machine without the kernel
being able to discover your key? IF NOT THEN YOU CANNOT DO REMOTE
ATTESTATION. The word "TPM" is not a magic security bullet that you can
use as a stopgap for when you want secure attestation but don't have
full Palladium support.

Unfortunately for most presenters the DARPA PR team was on HIGH ALERT so
a lot of the presentations had to be canned, but our elevator pitch was
essentially that ILLITHID finds vulnerabilities via magic. Frankly a lot
of the SMT work is magic even to me, but if I had to claim the two
pieces of magic in ILLITHID, they'd be the integration of human
understanding into the analysis of the system as a whole, and of course,
the ability for the system to use the SMT solver to find bugs. Finding
bugs with an SMT server is more than just doing symbolic execution the
way people do to find ROP gadgets. It requires a memory model, which is
a very tricky thing to get right. If you've looked at the images we've
posted (or attended the Immunity Master Class this year), you've seen
that every access to memory is tracked in a very particular way, useful
only for bug finding (technically, useful only for a particular KIND of
bugfinding - future versions are going to need a per-bugclass memory
model).

One of the key things here is pointer aliasing, which is the team's
fancy way of saying that two different pointers are pointing to the same
object in memory.  Given that, plus the ability to solve for constraints
on a path, you can use the SMT solver to find double frees, a bug class
I did not realize would be something we could apply that particular
hammer to. And of course this will get you the input that will reach
that particular path which is useful as well.

Needless to say there are not a lot of DoD executives who want to hear
these gritty details, but they usually smiled and nodded at the right
points. We're thinking of throwing another master class in DC at some
point, so if you want to learn these sorts of things and play with
ILLITHID a bit, let me know! (One of the first exersizes is computing an
RSA private key from a partial information leak of it, Heartbleed style
- this is not a class for beginners. :>)

-dave
 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 196 bytes
Desc: OpenPGP digital signature
URL: <https://lists.immunityinc.com/pipermail/dailydave/attachments/20140529/3b6c1a70/attachment.sig>