<r​brunner7:monero.social> Meeting in a bit more than 1 hour

<j​berman:monero.social> github . com errors are increasing on my end, pretty annoying

<j​pk68:matrix.org> matrix.monero.social/_matrix/media/…matrix.org/HfEObUkvmovkOxYuXGjeAMWZ

<j​pk68:matrix.org> Getting this one too?

<s​needlewoods_xmr:matrix.org> me too

<j​berman:monero.social> yep

<r​brunner7:monero.social> Yes, and on several repositories not related to Monero as well. I think this time they have outdone themselves, congratulations.

<r​brunner7:monero.social> Maybe they started to vibe-code? "Eating their own dogfood" as it was called many years ago?

<j​pk68:matrix.org> Pretty sure Microslop has openly bragged about vibecoding their products now

<j​pk68:matrix.org> cnbc.com/2025/04/29/satya-nadella-s…icrosoft-code-is-written-by-ai.html

<r​brunner7:monero.social> Meeting time. Hello! (No link to the meeting's meta issue, because GitHub is borked right now)

<j​berman:monero.social> *waves*

<s​needlewoods_xmr:matrix.org> hey

Hi

<j​pk68:matrix.org> Hello

<r​brunner7:monero.social> Alright, what are the reports about last week? Me: Could continue a bit with implementing Polyseed for the CLI wallet

<k​oe000:matrix.org> Me: multisig slowly

<s​needlewoods_xmr:matrix.org> added struct to describe transfers: github.com/monero-project/monero/co…066515d54ba97a2be645b5d33e6bb803ba7

<s​needlewoods_xmr:matrix.org> (hopefully) as you rbrunner recommended/imagined

<s​needlewoods_xmr:matrix.org> also worked on some smaller reports and reviews

<j​pk68:matrix.org> Added support for standard I2P hostnames to the daemon (awaiting review); published an AUR package for Cuprate; attempted to improve fiat API support in the GUI

<j​berman:monero.social> me: mostly beta stressnet prep (binaries coming soonTM) and followup on PR's for release v0.18.5.0

<r​brunner7:monero.social> jpk68: Looks like you pick up speed :)

<j​effro256:monero.social> howdy

<r​brunner7:monero.social> So, if you hope for binaries soon, jberman , no real blockers left I guess?

<j​effro256:monero.social> me: also stressnet prep, plus some vuln handling

<j​berman:monero.social> a small log spam thing I've been discussing with jeffro, it's not a major blocker but I think would be nice to have done. And ofrn is still doing some testing AFAIK

<j​effro256:monero.social> Will have that done in the next couple hours btw

<r​brunner7:monero.social> I wonder how we will fare as an open source project in the light of a possible pick-up of AI found issues. Might get interesting, or maybe merely annoying if we have bad luck

<r​brunner7:monero.social> As I see it, we can't do anything pro-actively, just wait what will happen. I think more or less the whole IT scene is now waiting for how things will turn out security-wise.

we received like 30 reports in the past month

so far the AI reports have been a couple interesting things and lots of more or less irrelevant edge cases

<r​brunner7:monero.social> Was that above long-term average?

yes, previously it would be like 1 report per month

<r​brunner7:monero.social> Ah, you mean only the AI reports were 30?

<r​brunner7:monero.social> 1 per month - oh, ok

yes so 30x increase, though i assume we will have solved the low hanging fruits with the next release so let's see if the high amount of reports continue

<j​effro256:monero.social> seraphis-migration/monero #336

<j​pk68:matrix.org> jeffro256: Sorry for asking you this for the 10th time, but have you heard anything new from Ledger/Trezor?

<j​pk68:matrix.org> I also wonder if the Trezor dev who originally implemented support is aware of the possibility of opening a new CCS for it

to be precise he was never CCS funded, in the past Trezor paid for it

<j​effro256:monero.social> Unfortunately, nope

<r​brunner7:monero.social> I dimmly remember that with one of the two there is a potential problem with a new protocol that pretty complicated, the protocol to talk to the device?

<j​pk68:matrix.org> RIP

<j​pk68:matrix.org> Yeah, it's kind of ludicrous

<r​edsh4de:matrix.org> the protocol, for reference: github.com/trezor/trezor-firmware/b…in/docs/common/thp/specification.md

jeffro if you could prioritise 10431 and 10367 that would be great, last thing missing for the release

<j​pk68:matrix.org> They created a new protocol that can work over Bluetooth or (Web)USB, that includes a cusom NoiseXX handshake and like 4 different trasnport layers

<j​pk68:matrix.org> The spec document (linked above) is quite literally 10x longer than the 'legacy' one

<r​brunner7:monero.social> That does not sound good.

rbunner, re: the future of open source projects facing AI-found issues - that's where protocol modelling and formal verification come in!

<r​brunner7:monero.social> MarkoPohlo: Hmm, yes, but I guess anything in such a direction will take time, and quite some effort in itself

<r​brunner7:monero.social> Maybe stupid question, but was there a real *need* for a new protocol?

<j​pk68:matrix.org> No...

<r​brunner7:monero.social> You could get the suspicion that they don't want other apps talking to their devices that eagerly anymore ...

<j​pk68:matrix.org> They also advertise their new device as 'post-quantum' despite the fact that the THP (Trezor Host Protocol) in its current state uses ECDH

<j​pk68:matrix.org> I think this is pretty disingenuous

<j​effro256:monero.social> selsta: heard, ty will do that today

<j​pk68:matrix.org> Anyways, I've become sort of intrigued by how an implementation of this would work, and at first glance, it appears we would need to have some sort of abstraction layer that manages the encryption and state machine

<j​effro256:monero.social> Yeah that new protocol seems like it was born in committee hell. Hopefully, once we have Rust toolchain integration, we can simply use Trezor's Rust library

<j​effro256:monero.social> haven't looked into it though

<j​pk68:matrix.org> AFAIK Trezor doesn't have a Rust library for that. Just Python at the moment

<r​brunner7:monero.social> Ah, there is a Rust library that speaks the new protocol? That's at least a shimmer of hope

<j​pk68:matrix.org> There is a BTC-only third-party implementation of it, but it's third party

<j​pk68:matrix.org> and tobtoht has also said it would not be preferable to add more Rust crates

<j​effro256:monero.social> github.com/trezor/trezor-firmware/tree/main/rust/trezor-thp

<j​pk68:matrix.org> How did I now know about that, lmao

<j​pk68:matrix.org> Apologies :)

<j​effro256:monero.social> I also would prefer not to add more crates, but I would prefer less to spend a crap ton of time reinventing the wheel.

<r​brunner7:monero.social> Well, I understand reluctance for adding more dependencies, but maybe it will turn out to be the lesser evil. Somehow I don't see somebody doing that protocol in C++

<j​effro256:monero.social> Especially since Trezor THP is ridiculously complicated

<r​brunner7:monero.social> Complicated == hight potential for bugs. Just saying :)

<r​brunner7:monero.social> I would say what you want when you buy a hardware wallet is a solid step up in security. Maybe that is not that.

<j​pk68:matrix.org> The Rust library also doesn't have an insane amount of dependencies (11, to be exact)

<r​brunner7:monero.social> Alright, looks pretty bleak then. Do we have something else to discuss today?

<p​alinatolmach:matrix.org> It is, but FV is benefitting a lot from AI improvements in terms of proof generation and scalability. Having a protocol model also unlocks many downstream positive effects as it can serve as a reference for AI codege, audits, test generation, vulnerability detection, and so on

<p​alinatolmach:matrix.org> It is, but FV is benefitting a lot from AI improvements in terms of proof generation and scalability. Having a protocol model also unlocks many downstream positive effects as it can serve as a reference for AI codegen, audits, test generation, vulnerability detection, and so on

<r​brunner7:monero.social> Doesn't look like it. Thanks everybody for attending, read you again in 1 week!

<s​needlewoods_xmr:matrix.org> thanks everyone

<r​brunner7:monero.social> palinatolmach: I can't really see what you would want a "protocol model" for. Our node-to-node protocol?

<r​brunner7:monero.social> And how would such a model look? Do you have some already existing examples?

<o​frnxmr:monero.social> Yes sir

<r​brunner7:monero.social> Looks like they are on it: githubstatus.com

<p​alinatolmach:matrix.org> It can be more coarse or fine-grained - we can have a more fine-grained model targeting one component, e.g. node-to-node, Carrot, consensus can all be modeled. This model can then be used to formally verify against, but it also unlocks detailed bug finding, since you have a very high-fidelity reference to check against, and so it can also be used to generate higher quality code an<clipped mes

<p​alinatolmach:matrix.org> d tests with AI. It would also be useful as a reference for porting the code to another language, if needed. For just the verification though, with AI doing some of the proofs and existing tools like Aeneas for Rust, we can do source code-level verification in some cases, without the need for modeling. A higher-level model maps out how these different components (consensus, wallet<clipped mes

<p​alinatolmach:matrix.org> , mempool, etc) interact, which is used to prove security properties over this model itself, but also outlines the security assumptions on the boundaries between these parts of the system explicitly, which makes issues there harder to miss.

<p​alinatolmach:matrix.org> One example I can share is the Dafny model we've built for Optimism's Supernode: github.com/runtimeverification/_aud…ny-models/op-supernode/dafny-models. It's still being worked on, but it has uncovered some simplifications in the design and code architecture, and just generally improving the quality of the audit we've don<clipped mes

<p​alinatolmach:matrix.org> e by feeding as context to AI agents we've used for assisting the review; that's in addition to verifying security properties over this model.

<p​alinatolmach:matrix.org> It can be more coarse or fine-grained - we can have a more fine-grained model targeting one component, e.g. node-to-node, Carrot, consensus can all be modeled. This model can then be used to formally verify against, but it also unlocks detailed bug finding, since you have a very high-fidelity reference to check against, and so it can also be used to generate higher quality code an<clipped mes

<p​alinatolmach:matrix.org> d tests with AI. It would also be useful as a reference for porting the code to another language, if needed. For just the verification though, with AI doing some of the proofs and existing tools like Aeneas for Rust, we can do source code-level verification in some cases, without the need for modeling. A higher-level model maps out how these different components (consensus, wallet<clipped mes

<p​alinatolmach:matrix.org> , mempool, etc) interact, which is used to prove security properties over this model itself, but also outlines the security assumptions on the boundaries between these parts of the system explicitly, which makes issues there harder to miss.

<p​alinatolmach:matrix.org> One example I can share is the Dafny model we've built for Optimism's Supernode: github.com/runtimeverification\_audits\_Ethereum-optimism\_optimism\_interopv2/tree/rv/dafny-models/op-supernode/dafny-models. It's still being worked on, but it has uncovered some simplifications in the design and code architecture, and just generally improved the quality of the audit we've <clipped mes

<p​alinatolmach:matrix.org> done by feeding as context to AI agents we've used for assisting the review; that's in addition to verifying security properties over this model.

<p​alinatolmach:matrix.org> It can be more coarse or fine-grained - we can have a more fine-grained model targeting one component, e.g. node-to-node, Carrot, consensus can all be modeled. This model can then be used to formally verify against, but it also unlocks detailed bug finding, since you have a very high-fidelity reference to check against, and so it can also be used to generate higher quality code an<clipped mes

<p​alinatolmach:matrix.org> d tests with AI. It would also be useful as a reference for porting the code to another language, if needed. For just the verification though, with AI doing some of the proofs and existing tools like Aeneas for Rust, we can do source code-level verification in some cases, without the need for modeling. A higher-level model maps out how these different components (consensus, wallet<clipped mes

<p​alinatolmach:matrix.org> , mempool, etc) interact, which is used to prove security properties over this model itself, but also outlines the security assumptions on the boundaries between these parts of the system explicitly, which makes issues there harder to miss.

<p​alinatolmach:matrix.org> One example I can share is the Dafny model we've built for Optimism's Supernode: github.com/runtimeverification\_audits\_Ethereum-optimism\_optimism\_interopv2/tree/rv/dafny-models/op-supernode/dafny-models. It's still being worked on, but it has uncovered some simplifications in the design and code architecture, and just generally improved the quality of the audit we've <clipped mes

<p​alinatolmach:matrix.org> done by feeding as context to AI agents we've used for assisting the review; that's in addition to verifying security properties over this model.

<p​alinatolmach:matrix.org> It can be more coarse or fine-grained - we can have a more fine-grained model targeting one component, e.g. node-to-node, Carrot, consensus can all be modeled. This model can then be used to formally verify against, but it also unlocks detailed bug finding, since you have a very high-fidelity reference to check against, and so it can also be used to generate higher quality code an<clipped mes

<p​alinatolmach:matrix.org> d tests with AI. It would also be useful as a reference for porting the code to another language, if needed. For just the verification though, with AI doing some of the proofs and existing tools like Aeneas for Rust, we can do source code-level verification in some cases, without the need for modeling. A higher-level model maps out how these different components (consensus, wallet<clipped mes

<p​alinatolmach:matrix.org> , mempool, etc) interact, which is used to prove security properties over this model itself, but also outlines the security assumptions on the boundaries between these parts of the system explicitly, which makes issues there harder to miss.

<p​alinatolmach:matrix.org> One example I can share is the Dafny model we've built for Optimism's Supernode: github.com/runtimeverification\_audits\_Ethereum-optimism\_optimism\_interopv2/tree/rv/dafny-models/op-supernode/dafny-models. It's still being worked on, but it has uncovered some simplifications in the design and code architecture, and just generally improved the quality of the audit we've <clipped mes

<p​alinatolmach:matrix.org> done by feeding as context to AI agents we've used for assisting the review; that's in addition to verifying security properties over this model.

<p​alinatolmach:matrix.org> It can be more coarse or fine-grained - we can have a more fine-grained model targeting one component, e.g. node-to-node, Carrot, consensus can all be modeled. This model can then be used to formally verify against, but it also unlocks detailed bug finding, since you have a very high-fidelity reference to check against, and so it can also be used to generate higher quality code an<clipped mes

<p​alinatolmach:matrix.org> d tests with AI. It would also be useful as a reference for porting the code to another language, if needed. For just the verification though, with AI doing some of the proofs and existing tools like Aeneas for Rust, we can do source code-level verification in some cases, without the need for modeling. A higher-level model maps out how these different components (consensus, wallet<clipped mes

<p​alinatolmach:matrix.org> , mempool, etc) interact, which is used to prove security properties over this model itself, but also outlines the security assumptions on the boundaries between these parts of the system explicitly, which makes issues there harder to miss.

<p​alinatolmach:matrix.org> One example I can share is the Dafny model we've built for Optimism's Supernode: github.com/runtimeverification\_audits\_Ethereum-optimism\_optimism\_interopv2/tree/rv/dafny-models/op-supernode/dafny-models. It's still being worked on, but it has uncovered some simplifications in the design and code architecture, and just generally improved the quality of the audit we've <clipped mes

<p​alinatolmach:matrix.org> done by feeding as context to AI agents we've used for assisting the review; that's in addition to verifying security properties over this model.