Share this page!

Brendan Dolan-Gavitt Profile picture
Twitter logo
19 Oct, 4 tweets, 2 min read
KLEE misses this UAF under a very weird set of conditions. Tried to use creduce but I couldn't figure out a nice way to force it to preserve the UAF when reducing. #include <stdio.h> #include <stdlib.h> #include <string.h> Test case reduction notes: * If puts(s) is directly after t
Reported here: github.com/klee/klee/issu…
Finally got creduce to work – apparently the if and the for loop are indeed crucial. creduce script on the right #include <stdio.h> #include <stdlib.h> char *a() { char b;#!/bin/bash T=$(mktemp) clang -Werror -g -fsanitize=address
It did also accidentally find this other KLEE crash though. Pretty sure it's a trivial bug though, caused by calling free() with no arguments.

• • •

Missing some Tweet in this thread? You can try to force a refresh
　

Keep Current with Brendan Dolan-Gavitt

Brendan Dolan-Gavitt Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!

PDF

Twitter may remove this content at anytime! Save it as PDF for later use!

Try unrolling a thread yourself!

how to unroll video
  1. Follow @ThreadReaderApp to mention us!

  2. From a Twitter thread mention us with a keyword "unroll"
@threadreaderapp unroll

Practice here first or read more on our help page!

More from @moyix

Brendan Dolan-Gavitt Profile picture
10 Sep
Excited to announce that registrations are open for ChaffCTF, a small CTF built around chaff bugs! The CTF will run from Sep 24-26 chaffctf.com
If you don't remember what Chaff Bugs are, you can check out our paper: arxiv.org/abs/1808.00659
Or this article from 2018: vice.com/en/article/43p…
Read 4 tweets
Brendan Dolan-Gavitt Profile picture
2 Sep
While I wait for the GPU to churn through 2*26^11 possibilities, a brief recap of how we got here. It started when I noticed this bit of code in the @GitHubCopilot Visual Studio Code extension that detects naughty words in either the prompt or the suggestions. Screenshot of the Github Co...
Because the words are hashed, we have to guess what words might be in the list, compute the hash of each, and then check to see if it's in the list (just like cracking password hashes).
This managed to decode about 75% of the list right off the bat, and turned up some weird entries, like "israel" and "communist"
Read 21 tweets
Brendan Dolan-Gavitt Profile picture
2 Sep
After scoring the 854,653 solutions found by the CUDA hash cracker using GPT-2, I believe we have solved another two of the remaining slurs - the highlighted word and its plural! (The scores here are log-probabilities) whartinkala -38.659 jfraskeride -38.49 actnopathik
Only two hashes are left uncracked:

272617466 and 867567715

Good thing I have two GPUs 😎
(To be scrupulously fair I suspect a couple of the "decoded" entries on the list, like "w00se" and "jui ch", are collisions. But I have to draw the line somewhere.)
Read 5 tweets
Brendan Dolan-Gavitt Profile picture
1 Sep
TFW you're happy that your GPU-accelerated hash finder gets 24 million hashes/sec but then you remember hashcat can do ~65 BILLION MD5 hashes/sec on the same device...
If anyone would like to tell me how hashcat manages to pull off this feat I'd be super curious, 3000X faster is a LOT (and MD5 is more complex than the function I'm trying to compute!)
Current code if anyone wants to take a look gist.github.com/moyix/f78e0b0d…
Read 4 tweets
Brendan Dolan-Gavitt Profile picture
1 Sep
I feel like I always get tripped up on silly things with CUDA – like: I can compute all these results very fast, but actually saving and reporting them somewhere is a huge pain.
Either I just call printf() device-side and tank performance or I have to manage parallel host and device buffers, synchronize between GPU threads for adding things to the result list and lose the ability to see results as they come in.
Here's what I'm trying to implement now but it seems more complex than it ought to be... stackoverflow.com/questions/2034…
Read 5 tweets
Brendan Dolan-Gavitt Profile picture
30 Aug
Question for Z3Py experts: my model has an Array assignment like this:

[word0 = Store(Store(Store(Store(Store(K(BitVec(32), 107), 3, 110), 6, 0), 0, 115), 2, 97), 4, 99)]

How can I add its negation (Or(word0[i] != model[word0[i]]) for i in range(arraylen)) to the constraints?
Unfortunately since the constraints were loaded in from an SMT file I don't have the original Array, nor do I know how to retrieve it from the constraint object or model...
Ok this just feels cheeky: I asked Z3 for an array word0 where word0 != FirstSolution. It happily provided me with such an array: FirstSolution but with array index 1073741824 set to 64. This is how I learned Z3 has no concept of array length.
Read 7 tweets

Did Thread Reader help you today?

Support us! We are indie developers!

This site is made by just two indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3/month or $30/year) and get exclusive features!

Become Premium

Too expensive? Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal Become our Patreon

Thank you for your support!

Follow Us on Twitter!

Like this author's thread?

Get emails when @moyix has new unrolls!

Check out other threads from @moyix!

Read all threads by @moyix

:(