Trustless TEE and DevProof

I'm giving a very quick overview. So I'm choosing, like, a specific sliver of this topic to talk about.

I'm assuming everyone kind of knows what, what TEEs are. So, I think everyone will agree that we're entering a world in which, coordination between multiple agents, algorithmic or human, is just gonna... Is, is exploding already and happening at a much, much faster pace than what we're used to. Everything's happening at, like, millisecond machine speed. To, you know, have privacy, to, have efficient interactions, we cannot rely on legal guarantees in this space. It's just way too slow and inefficient. And TEEs are this interesting technology that, I think broadly will shape the way in which, these kind of interactions happen by allowing people to sort of, trust their counterparties without signing contracts, to very precisely control how their data is used.

And we've seen so many TEE talks. I think we, can all agree that TEEs are gonna be a big part of the future. And, really what TEEs do is they, take this, like, single actor we think of as our, like, trusted counterparty, like the developer of the platform that I'm using, like Google or whatever, and they maybe remove some of their control to make it, to make it dev-proof in some sense. But really what's happening is that we're just taking away some of the trust assumptions. And there is still a large and significant residue, and, it highlights some of the other assumptions that we're making. So, you know, in relying on the security of a TEE, you're relying that the attested logic is secure and bug-free and not backdoored.

Obviously, you'd be able to... You know, it would have to be a hidden backdoor. You're making similar assumptions for the chip itself. You know, the chips can be backdoored. Chips can be, attacked with, like, physical attacks where people monitor power usage and, all sorts of, instruction sequences to extract, your private keys, your information from these kinds of machines. And, you know, usually the talk that I give is, like, TEE are a huge part of the future. The situation is dire, and we really need to pay attention to this, and here are, like, these deep technical things that need to happen that cost billions of dollars to, like, move the needle. But that picture has kind of changed.

So, I spoke about power, power side channels as a couple of different examples of ways information can be extracted from these TEEs. And this is, well, not a real graph, but, this is kind of what a power trace will look like of a, of a chip running over different kinds of private data. And in the deviations in this power usage actually lie a lot of your private data. And, it's like there's a whole field of academics, academia studying how to extract keys and other kinds of information using these kinds of power traces.

But the cool thing... Oh, and, the, reason that, this hasn't been addressed, I mean, partly is, like, overhead and these kind of things, but it's also just because the industry incentives haven't been there. There's a couple of very large, well-capitalized companies that do most of the Have That, like, steer the chip world in one way or another, and they never have had the incentives to build a very powerful but secure machine, a, like, Trustless TEE in some sense. But a lot of the barriers to actually working on this kind of technology have fallen away, in recent years and partly due to AI. So you might have seen in the Kimi, Kimi K3 model announcement, they spoke about how in forty-eight hours they could design, or Kimi could design a AI accelerator chip.

And what's really missing now is the security properties. But as much as I was talking about physical security properties, a lot of this can be addressed in software. So, fortunately, over the last ten years there's been this, like, field of academia that's been trying to make the physical security properties and other side side-channel security properties of chips digitally checkable. And what's now become possible is we can take our models and feed them these tools and actually, like, drive at this frontier of what secure hardware is today and vibe code secure chips. And the, this chart on the left is from a paper where some people figured out, like, okay, we can formally verify the security properties we need.

Now we just need to basically throw compute at it to, get the optimal kind of chip design within this.

And there's been a lot of... Or maybe in my world, there's been a lot of, like, competitions to make, SNARKs more efficient. To throw your models at, like, circuits and proven lean if they're correct and make things more efficient. We can do the same for hardware. And, yeah, I think that's a, like, a weird, vibe coding project that I wanna to challenge people to maybe pick up or in a couple of months pick up and it's easier to do.

So you've vibe coded your own, like, secure chip already? Like, you've already designed a chip through vibe coding that does SGX or whatever enclave type things?

It's actually an ongoing project I have right now. So making chips, not that hard.

The, a lot of the tools, do like exhaustive checks of the circuits. And, then you have composability properties, so you prove one thing exhaustively, and then you say, "Okay, if I compose these, I preserve the properties." But the expensive thing is doing the initial proof, and I'm converting all of that into lean.

And so that side of things has been slow, but I'm making progress, yeah.

I mean, so if this, vibe coding chips and then formally proving them goes well, how optimistic about you, are you about the possibility that you'd be able to vibe code, like, either GDS or, like, even much lower levels of chip design and then just get rid of a whole bunch of proprietary chip software?

So there's, like, multiple levels to the chip design flow. One is, like, just getting the digital description of the chip down. You know, like, we know that, you know those diagrams, the AND, the OR, and the whatever gates. And then there's another step which goes from that to, like, the actual physical design, which is super detailed, and you get these, like, 3D models at the end called GDSs.

I am very optimistic. I, I've heard, like, the open EDA, like, silicon design ecosystem has got a lot of attention from companies training models, to do chip design. Some of the EDA flow is just computationally bottlenecked. But that bottleneck is way less tight than the current, like, commercial grip of the proprietary companies. So, let's say you want to design a chip, Synopsys or Cadence, one of these EDA companies, will charge you per core that you run their software on. So if you want to scale that up and have a model have, do 20 attempts at once, you have to pay 20 times as much. And it's an exorbitant amount. Whereas with open silicon, you just have to pay for the...

Of open design tools, you just have to pay for the compute, which is much cheaper and scales much better. So yeah, very excited.