Has anyone tried throwing AI at the problem?

I'm sure they have. But yea, it's a delicate thing and there are no low hanging fruits left. Probably not even any medium hanging fruits either.

Good work! Has anyone tried throwing AI at the problem? This is the sort of thing that it's really good at... Although I guess normally that's because there's a lot of medium hanging fruit that people haven't had time to look at, whereas the Rust compiler is very mature. Still, definitely worth a try. Anyone from Anthropic or OpenAI here? I have unlimited tokens at work but unfortunately I don't use Rust.

I really like how the Rust developers looked at prior art, and combined some of the best ideas from various sources into something new. Traits are basically Haskell type classes. They're modified a bit to allow fluent method chaining; but you can still call trait methods via the trait reference which is the Haskell style. Associated types in traits match up with one half of the functionality from GHC's Type Family language extension.

Enums, the Option and Result types, and pattern matching come directly from the ML language family. Hygienic macros also have roots in functional programming.

Iterators bear a passing resemblance to Haskell's lazily-evaluated lists. In both cases you can pile on transformations without intermediate allocations. But of course the implementations are very different.

• Fixed "Illegal instruction" error on certain x86_64 CPUs without SSE4.1. pr#5162
• Fixed "lock() not supported" error on Solaris. pr#5167

Further details are available in the changelog!

me follows link to changelog, same two list items

Here are the top 5

The top 5 what?

The top 5 features. I wouldn't say that the article is a pinnacle of writing, but it feels like:

• you haven't read it

• LLMs would not write it so chaotic

Ugh I really wish they'd support something less awful than GNU linker scripts. You should be able to write linker scripts in Starlark or something.

Might have helped the introduction if you said what you are talking about...

Here are the top 5

The top 5 what?

Looks like it should just work, right? On stable it doesn't, and it trips twice.

"Trips" does it Claude? 🤨

No problem. It’s a surprisingly good tool despite relying completely on hallucination machines.

Thanks! This is very helpful! I'll take a look and fix it.

I used a frontier model to generate an allium spec from your repo and it found a few bugs. I like to run apps through allium to prepare for formal verification because it tends to find a LOT of flaws in even the most robust apps. The allium spec file is too large to share here but it can be generated by any frontier model.

Defects, three of them confirmed by running probes against the crate:

• P1, a late message from the previous chain breaks the session. The decrypt code never keeps the leftover keys of the old receiving chain, and it reads the header's previous chain length only as associated data. So a delayed message from the old chain looks like a new ratchet key. The session steps the ratchet again and the tag fails. In the probe, the next good message also failed with an AES-GCM error. Signal handles exactly this case, and the crate's out-of-order test only reorders messages within one chain.
• P2, one forged message with a made-up ratchet key desyncs the session for good. The ratchet step and key skipping happen before the tag is checked, and they're never rolled back. In the probe, the next real message failed.
• P3, a forged message naming a skipped key deletes that key before the tag check. The real message then fails with "Message number mismatch".
• The signed prekey's signature is never checked. x3dh_initiate_internal doesn't call verify_signed_prekey, and the WASM API doesn't expose it. Prekey authentication depends on every application remembering to do it.
• The X3DH associated data isn't bound to the two identities. It's the constant "X3DH_Key_Exchange" rather than both identity keys, and the ratchet never uses it anyway.
• The identity key and the signing key are unrelated. It uses a separate, unbound Ed25519 signing key instead of XEdDSA on the identity key.
• The first chain gets no DH ratchet. On both sides it's derived from the X3DH secret alone.
• Smaller issues:
• • There's no cap on the total number of skipped keys.
  • Cleanup drops keys in string order, not oldest first.
  • The send counter is a u32 with no overflow check.
  • The DH output isn't checked for all-zero values from small-order keys.
  • The legacy encrypt_message helper returns the message key to JavaScript. Variants, not defects: the non-standard HKDF salts and info strings. Both sides agree on them, and the spec says so.

-- VIOLATED: only one decrypt's skip is capped (max_skip); nothing caps
-- the total unless the application calls cleanup, so a peer that keeps
-- skipping grows the state without limit.
invariant SkippedKeysAreBounded {
    for s in Sessions:
        s.skipped.count <= config.max_skipped_total
}

invariant OneTimePreKeysBelongToOneSession {
    for a in Handshakes:
        for b in Handshakes:
            a != b and a.one_time_prekey != null
                implies a.one_time_prekey != b.one_time_prekey
}

invariant ResponderCannotSendBeforeReceiving {
    for s in Sessions:
        s.role = responder and s.receiving_ratchet_public = null
            implies s.sending_chain_key = null
}

open question "Should x3dh_initiate_internal take the signing key and signature and verify the signed prekey itself, so a caller cannot skip it?"

open question "Should the identity key sign with XEdDSA, so there is one long-term key instead of an unbound X25519 and Ed25519 pair?"

open question "Should decrypt work on a copy of the state and commit only after the tag verifies?"

open question "Should the associated data be IK_A || IK_B and be passed into every seal and open?"

Similar Signal rust projects:

https://github.com/wnoronha/signal-cli

https://github.com/foxl-ai/signal-cli

Did you remember this time to tell copilot to actually write stuff in the files and not just create them?

the typical software development approach: unit tests, reviewing PR changes, documenting details and CI/CD (to mention a few steps). its not something i can easily enumerate because in cybersecurity there are countless nuances to consider, which is how we end up with formal verification documents and security audits. all the internal documents are useful for me, but essentially geared toward being a starting point for a third-party reviewer.

the impementation here is being used in a couple functional messaging apps (similarly unaudited and unreviewed):

• https://enkrypted.chat/ - javascript based approach
• https://glitr.io/ - rust based approach

i will also be adding it to an open source project soon as seen at: https://github.com/positive-intentions/chat to give that e2e open-source transparency in the implementation.

I mean on code level. How did you make sure, the LLM prints out something maintainable, understandable?

thats right. i used LLM's. i reviewed this thoroughly myself. there are some in-house documents published on the website. for exmples threat-models, formal-verification and security audits. they are good for internal review but fundamentally invalid because its like "trust me bro"... and you shouldnt need to.

i would like to aim for a third-party review from an org like ROS or NLNet, but open source support isnt easy to come by on project as complicated as this. im sure many orgs are overwhelmed by AI slop and i've failed to make the cut several times, so im not expecting a professiona audit any time soon.

feel free to reach out for clarity on the details if you would like to investigate it further.

All of these sound amazing tbh!

You used LLMs, right?

How did you manage to review all this?

Google has a single massive monorepo with excellent search, reuse, and build caching. Keeping modules small so they are easy to test, review, update and reuse makes a lot of sense with that kind of infrastructure.

The rules of no directories and super-small crates seem kinda silly to me but I guess Google's build system is special enough that it makes sense for them.

Huge thanks for sharing what you know about the project!! ❤️

As for the part on what "will" happen though - you're free to subscribe to your set of beliefs about the future; mine are respectfully different, and my question stands! 🙃

The project has been around for a while, so the progress hasn't been vibe-fast, I would say.

It's not obviously vibe-coded from what I can tell, although they did embrace "AI" help early on (e.g. copilot reviews).

Utilizing AI in one or more ways is becoming the norm, irrespective of how we feel about it. So the practical question will increasingly become: how competent/knowledgeable are the developers driving a project, not how manual is their development.

The people behind Asterinas are not random enthusiastic youngsters. And some of what they do is original anyway.

Whoah, that's something! 🤯

And there's even a very nice and interesting LWN writeup about it from a year ago: https://lwn.net/Articles/1022920/ - looks legit and, for now, the more I read the more interested I am!

I wonder how much vibecoded it is, though? The speed they seem to progress at feels impressive on the surface

cross requires Docker which is a really awkward dependency, especially on Windows and Mac, or if you're already in Docker, e.g. in CI or a dev container.

Plus it's quite slow. Cargo zigbuild was a much nicer solution when I finally resorted to it. Zig is easy to install, even on Debian - just download and untar.

I only managed to do it thanks to cargo zigbuild which is amazing. (And kind of embarrassing that Rust has to use Zig to get a nice cross-compiling UX, but hey it works.)

As in cross didn't work for this?

aws-lc-rs is probably the most popular but also quite annoying because it uses C, so cross-compiling is a bit of a pain. I only managed to do it thanks to cargo zigbuild which is amazing. (And kind of embarrassing that Rust has to use Zig to get a nice cross-compiling UX, but hey it works.)

The other one is ring, which I'm not really sure the status of but I recall they had some super weird versioning policies that weren't very popular.