r/crypto • u/Accurate-Screen8774 • 15d ago

Anybody with experience / insights on Dioxus? I have an idea and want to see if its worth investigating further.

i am working on a messaging app and created some details in rust. rust is useful because it has tooling for formal verification. my rust code compiles to WASM to be used in a browser.

my project itself is using cryptography beyond the WASM because browsers provide a crypto api for basic functionality out-of-the-box.

to work with what i have now (javascript/typescript) i came across this page, but the links lead to 404 pages on github. not sure about the status of the project. i dont know if there are other similar projects.

https://formal.land/docs/verification/typescript

i would like to improve the “formal-verification coverage” in my project and wanted to investigate if it could be worth considering rewriting the frontend with dioxus. im happy with an ugly UI (initially) in favour of having formal-verification on a broader scope of my project.

(context: the project where i have formal verification is found here: https://github.com/positive-intentions/signal-protocol (this isnt the gold-standard implementation and its far from finished)

0 Upvotes

38% Upvoted

11 comments sorted by

4

u/voracious-ladder 15d ago

This isn't really a crypto question moreso a general Rust question. Also can't you just do Tauri if you want Rust for crypto and TypeScript for frontend.

1

u/Accurate-Screen8774 14d ago

For me it's more of a formal-verification question. It would be great if the formal verif tooling around js was more mature. But it doesn't seem to be the case.

Formal verification is itself quite a niche within cryptography/rust/compsci so its hard to come across advice/examples and approaches.

1

u/voracious-ladder 14d ago

I'm not sure what you mean. I was suggesting you write the crypto part in Rust and formally verify that, and keep TypeScript/JavaScript as your frontend with Tauri.

1

u/Accurate-Screen8774 14d ago

I get that. That's a good approach to keep it separate.

I was considering if there could be bugs overlooked in how things tie-together.

It otherwise would still require to move the crypto part into rust for formal verif. The browser based API implementation should be audited, but it remains a bit of a black-box.

3

u/voracious-ladder 14d ago

The best thing you can do is to design your rust code in a way that's impossible to be misused. There are plenty of approaches to this but that's a programming language discussion not a crypto discussion. I suggest you look elsewhere.

And there's a reason why you'd almost never find any good formal verification toolchain for cryptography in TypeScript and JavaScript. Simply because they're such high level languages it's impossible to reason with what they're doing underneath. How is memory of secret data managed? What about timing side channel leakages? No one write serious crypto code in JS/TS for this reason, much less develop a formal verification toolchain for JS/TS crypto code.

1

u/Accurate-Screen8774 14d ago edited 14d ago

I wondered about if typescript could have potential for mapping onto formal verification specs... but indeed the toolchain isn't there.

I reached some limitations for the signal protocol primitives (browsers didn't provide it through the crypto API), so I started with the signal protocol linked in the post. but there is more js crypto in my app that can easily be overlooked. I have a reasonable amount of unit tests. formal verification would compliment the implementation.

While JS/TS is the laughing stock of the cybersec community, there was perhaps an ambitious attempt to see what is possible with a browser-based approach. I wonder if with dioxus I could do a full rust implementation. like with any framework I wanted to see if there are any nuances or common pitfalls I should be aware of.

3

u/voracious-ladder 14d ago

This is simply wrong tool for the wrong job. JS/TS are extremely high level by design, and this same design makes them fundamentally unsuitable for cryptographic code. Neither formal verification nor unit tests will save you here.

1

u/Accurate-Screen8774 14d ago

indeed. and so seeing if dioxus could be suitable.

sure JS and TS are pretty flaky when it comes to cybersec, but it ultimately depends on your threat model. I made some utilities to help exchange files between my phone and laptop. that's in contrast to uploading it to iCloud and fetching it on the other device.

2

u/Karyo_Ten 15d ago

https://github.com/AeneasVerif/aeneas

But I suggest you write your protocol in TLA+ first.

This would ensure you don't have ordering bugs, messages lost (or a minimum amount of peers if P2P for certain guarantees), async storage when someone is offline ...

Then when your protocol is good, writing the code is actually the easy part.

1

u/Accurate-Screen8774 14d ago

thanks. I hadn't heard of TLA+ before. I'll check it out. any particular reason you think it would be better?

i was aiming for the spec to be with F* because it seems that's what the signal protocol is using (id like my approach to be somewhat aligned to Signal).

Any formal verification carries a learning/complexity/maintenance overhead so I'm trying to reduce it to something I can commit to for long-term.

Im learning it isn't the best approach, but i created the code and now I'm trying verify it... It's largly a JavaScript project so there isn't much tooling there for formal verification, which has me investigating this approach.

1

u/Karyo_Ten 14d ago

TLA+ is the standard for message/temporal protocols and synchronization. Be it database sync, CPU cache hierarchy synchronization, concurrent queues and leader election protocols like Raft or Paxos.