laginimaineb

To name a couple.

(a) Scope: Maxwell can optimise portions of both your own code, but also of underlying libraries too (think libc), according to your data flow and env. These aren't places where you necessarily have source code or an easy way to replace it.

(b) It's dynamic: like a JIT, if your data flow _changes_, Maxwell detects new bottlenecks and reoptimises. A good example is an inference pipeline where e.g. the concurrency or seqlens can change suddenly (depending on what your users do). If you reoptimise for each such case, you'll do so forever (and there are many different operational points, each requiring their own algorithmic approach).

Uhm I wrote the blog, and I'm quite proud to say it is human written... And nowhere did I say anything about AI assistance. Happy to address any questions about substance if you like.

I don't follow.

If you don't use Maxwell everything works as is.

Maxwell does swaps in memory during runtime, not on disk.

And we of course sign every output and do externalise the proof of equivalence.

Actually Maxwell can reuse optimisations across users by clever caching. (A cool side effect is that the more it is used, the faster it becomes for everyone).

Bend is a formal language, but its use is quite different (also, Bend is much too narrow for Maxwell's use case...).

We need proofs of equivalence (including for code with side effects!) between original code, and new code, possibly in some other language. Say Python and a raw SIMD implementation. To do this we have a full 'embedding' of said languages in the same formal framework. It also requires modeling exactly what 'state' means in dynamic high level languages.

That gets you nowhere near the same level of acceleration.

More technical details forthcoming of course, including about formalisation... We indeed do not redo the same work over and over, but rather cache intelligently. We take special care not to interfere with debugging workflows (much in the same way that, e.g., the Tier 2 JIT does, in CPython). And as for visibility into the level of source code, what do you mean? The rewritten binary portions don't always have associated code, let alone in the language of origin.

Yes, CEMs can also help reduce bugs. To give an example, we found several memory safety bugs in core CPython code, through our formalisation. We'll release more details on that soon.

The verification is, which allows the optimisation to be extremely broad and non deterministic.

It's really unlike a compiler. For example, for a function like 'sort', the optimisation can:

- Use quicksort if the data distribution is generic.

- Use insertion sort if the data is nearly sorted

And so on... As long as these can be proven sound, Maxwell can pick the best optimisation in real time.

(I work at doubleAI.) The benchmark numbers (90% wins, 2.24x speedup on average, with key attention workloads accelerated ~15x) are one part of the story. The other: AI-generated kernels can pass simple verifiers with room to spare and still break in production. Our writeup walks through one such case: a fused embedding-gradient + RMSNorm backward kernel. As an example, we took the fastest (highest scoring) submission on the benchmark, for this task, submitted by other competitors, put it in our training code, and... everything broke (the loss diverged). The bug turned out to be subtle and hard to nail down (even changing the input distribution or the optimiser made it invisible). More details are in our blogpost.

We find these kinds of bugs very interesting: defending against humans is not the same problem as defending against agents. As models are becoming more powerful, they're also getting great at subverting verifiers (going through the 'path of least resistance'). This means that stronger verifiers are becoming increasingly more necessary, something we at doubleAI specialise in. You can also read our previous blogposts where we discuss this.

Happy to answer technical questions.

Actually, I would imagine they are nothing like one another.

However, Exynos uses a TrustZone TEE implementation to implement the KeyMaster module, just like Qualcomm's Snapdragon. This means that unless that TEE implementation uses a hardware key which is not software accessible, the same issue would be present. Of course, reverse-engineering a new TEE implementation would take a long time... But it sounds like it could be fun.

You're right. Let's take a second to go over the issues:

1. The arbitrary code-execution in TZ has already been privately disclosed and fixed.

2. As for the second issue - I would argue that it's not an issue at all. TZ should be updated (otherwise how would they fix the TZ code-exec vulnerabilities?).

However, in this case gaining code execution in the TZ kernel directly leads to the disclosure of the keys which are meant to bind the KDF to your device. This is in direct contract with Apple's KDF. The key here is that software shouldn't be trusted, by design.

3. As for the last issue, I would argue that this is just a clever form of social-engineering. After all, who's to say they didn't just swap the phone with a dummy phone to make you insert the correct password?

However, in Android's case, you wouldn't even need to cooperate. OEMs could simply flash the new TZ code, extract the KeyMaster keys, and bruteforce the key. All without having any help from you.

I believe so.

I'll definitely try and get around to it sometime soon. However, I wouldn't be surprised if the situation is the same... After all, the KeyMaster module was initially only meant to keep encryption keys on the device, not to safeguard FDE.

FWIW, formal verification requires a complete and exact spec - the TZ kernel is very complex and interacts with nearly all the peripherals on the SoC, it doesn't just manage QSEE applications. I think creating a spec for something like that would be really hard.

Widevine DRM is integrated into virtually all Android phones. If you're building your own ROM, you could remove the widevine.bXX files from the ROM image itself - I've never tested it, but it could probably soft-fail. There's no other way to remove it.

Anyway, this specific issue has already been fixed (but there are probably more bugs lurking either there on in other trustlets).

I believe so

Don't think I'll collect it, but I will release all the details so people can do it themselves.

It will work on the Turbo! :)

But you'll either need a version old enough to be vulnerable to this TrustZone exploit, or you can wait a couple of weeks until I release a new exploit (which also works on the Turbo).

Thanks! I'm also on twitter in case that helps (@laginimaineb).

As for Sunshine - I'm publishing a new (even broader) zero-to-TZ saga, complete with exploits, but I'm not going to create a product out of it. So ultimately, as long as there are people behind Sunshine who are willing to make it work with relative ease, I'm sure most people won't mind spending a few dollars to unlock their device.

As for the more tech-savvy crowd; I hope they choose to do it themselves with the exploits provided - it is much more fun that way, IMHO.

AFAIK it's unknown - there's a controller on the SoC which is responsible for reading/writing the fuses, but its firmware is in mask ROM and isn't available. Perhaps it's a real chemical reaction? Maybe it's just emulated in firmware? Your guess is as good as mine.

In this case, it seems so. However, I must say I've reported many vulnerabilities to Google since and they've all been handled within that time-frame.

That's a great question! I didn't cover this in the blog post, but there is a primitive identical to the increment-by-one presented there, which allows me to decrement-by-one as well (I've gone into more detail in the exploit code: https://github.com/laginimaineb/cve-2014-7920-7921)

Thank you. Also, the map is mostly Thorin's, with only slight adaptations :)

Thanks! More to follow soon :)

Sure, see the first part of the blog post, under "Responsible Disclosure"

(Disclaimer: I'm the author of this blog) In this post I cover the development of a full TrustZone exploit in MSM8974 (Snapdragon 800) SoCs, resulting in arbitrary code execution in the "Secure World". I've also provided the full source code!

Please let me know if you have any questions/comments.

I've reversed those files in the past as well, and you're correct, they are TrustZone applications (like Widevine, DxDHCP, Keymaster and more). I have a script which can be used to reunite these pieces of code into an ELF file which can be loaded into IDA (more about this in about a month!)

Anyway, if you're looking to load arbitrary code into TZ, wait for the next blog post (approx. 2-3 days)!

Thanks for reading!

I haven't heard of such a project, but I'm not 100% sure I understand what you mean; are you asking if there are non-Android implementations on mediatek chips?

Actually, I haven't been able to write posts these five months because of the ongoing semester. The whole discovery to exploitation didn't take more than a week, AFAIR.

As for the next post (with full exploit code!), you can expect it within 3-4 days tops.