16:57:22 Meeting in a bit more than 1 hour 17:49:52 github . com errors are increasing on my end, pretty annoying 17:50:27 https://matrix.monero.social/_matrix/media/v1/download/matrix.org/HfEObUkvmovkOxYuXGjeAMWZ 17:50:28 Getting this one too? 17:50:55 me too 17:52:50 yep 17:55:41 Yes, and on several repositories not related to Monero as well. I think this time they have outdone themselves, congratulations. 17:56:22 Maybe they started to vibe-code? "Eating their own dogfood" as it was called many years ago? 17:57:22 Pretty sure Microslop has openly bragged about vibecoding their products now 17:57:22 https://www.cnbc.com/2025/04/29/satya-nadella-says-as-much-as-30percent-of-microsoft-code-is-written-by-ai.html 18:00:06 Meeting time. Hello! (No link to the meeting's meta issue, because GitHub is borked right now) 18:00:17 *waves* 18:00:24 hey 18:00:29 Hi 18:00:38 Hello 18:01:44 Alright, what are the reports about last week? Me: Could continue a bit with implementing Polyseed for the CLI wallet 18:02:07 Me: multisig slowly 18:02:22 added struct to describe transfers: https://github.com/monero-project/monero/compare/c233a3eff0721686a39f7bb363b57a53aa5a75b2..55d02066515d54ba97a2be645b5d33e6bb803ba7 18:02:24 (hopefully) as you rbrunner recommended/imagined 18:02:26 also worked on some smaller reports and reviews 18:02:32 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 18:02:55 me: mostly beta stressnet prep (binaries coming soonTM) and followup on PR's for release v0.18.5.0 18:02:57 jpk68: Looks like you pick up speed :) 18:03:32 howdy 18:04:56 So, if you hope for binaries soon, jberman , no real blockers left I guess? 18:04:57 me: also stressnet prep, plus some vuln handling 18:05:56 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 18:06:12 Will have that done in the next couple hours btw 18:06:37 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 18:07:57 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. 18:08:38 we received like 30 reports in the past month 18:08:52 so far the AI reports have been a couple interesting things and lots of more or less irrelevant edge cases 18:09:17 Was that above long-term average? 18:09:39 yes, previously it would be like 1 report per month 18:09:49 Ah, you mean only the AI reports were 30? 18:10:06 1 per month - oh, ok 18:10:44 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 18:11:39 https://github.com/seraphis-migration/monero/pull/336 18:12:45 jeffro256: Sorry for asking you this for the 10th time, but have you heard anything new from Ledger/Trezor? 18:13:23 I also wonder if the Trezor dev who originally implemented support is aware of the possibility of opening a new CCS for it 18:13:53 to be precise he was never CCS funded, in the past Trezor paid for it 18:14:16 Unfortunately, nope 18:14:21 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? 18:14:23 RIP 18:15:04 Yeah, it's kind of ludicrous 18:15:08 the protocol, for reference: https://github.com/trezor/trezor-firmware/blob/main/docs/common/thp/specification.md 18:15:43 jeffro if you could prioritise 10431 and 10367 that would be great, last thing missing for the release 18:16:02 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 18:16:21 The spec document (linked above) is quite literally 10x longer than the 'legacy' one 18:16:35 That does not sound good. 18:16:37 rbunner, re: the future of open source projects facing AI-found issues - that's where protocol modelling and formal verification come in! 18:17:40 MarkoPohlo: Hmm, yes, but I guess anything in such a direction will take time, and quite some effort in itself 18:18:19 Maybe stupid question, but was there a real *need* for a new protocol? 18:18:28 No... 18:19:05 You could get the suspicion that they don't want other apps talking to their devices that eagerly anymore ... 18:19:38 They also advertise their new device as 'post-quantum' despite the fact that the THP (Trezor Host Protocol) in its current state uses ECDH 18:20:16 I think this is pretty disingenuous 18:20:37 selsta: heard, ty will do that today 18:21:55 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 18:22:17 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 18:22:23 haven't looked into it though 18:22:55 AFAIK Trezor doesn't have a Rust library for that. Just Python at the moment 18:23:04 Ah, there is a Rust library that speaks the new protocol? That's at least a shimmer of hope 18:23:24 There is a BTC-only third-party implementation of it, but it's third party 18:23:35 and tobtoht has also said it would not be preferable to add more Rust crates 18:23:44 https://github.com/trezor/trezor-firmware/tree/main/rust/trezor-thp/ 18:24:17 How did I now know about that, lmao 18:24:22 Apologies :) 18:25:37 I also would prefer not to add more crates, but I would prefer less to spend a crap ton of time reinventing the wheel. 18:25:54 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++ 18:26:07 Especially since Trezor THP is ridiculously complicated 18:27:15 Complicated == hight potential for bugs. Just saying :) 18:27:59 I would say what you want when you buy a hardware wallet is a solid step up in security. Maybe that is not that. 18:29:01 The Rust library also doesn't have an insane amount of dependencies (11, to be exact) 18:29:14 Alright, looks pretty bleak then. Do we have something else to discuss today? 18:30:27 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 18:30:34 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 18:31:16 Doesn't look like it. Thanks everybody for attending, read you again in 1 week! 18:31:49 thanks everyone 18:32:42 palinatolmach: I can't really see what you would want a "protocol model" for. Our node-to-node protocol? 18:33:17 And how would such a model look? Do you have some already existing examples? 18:40:24 Yes sir 18:42:19 Looks like they are on it: https://www.githubstatus.com/ 19:00:46 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 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 , 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. 19:00:50 One example I can share is the Dafny model we've built for Optimism's Supernode: https://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 improving the quality of the audit we've don 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. 19:01:37 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 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 , 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. 19:01:42 One example I can share is the Dafny model we've built for Optimism's Supernode: https://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 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. 19:02:10 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 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 , 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. 19:02:14 One example I can share is the Dafny model we've built for Optimism's Supernode: https://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 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. 19:02:18 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 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 , 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. 19:02:24 One example I can share is the Dafny model we've built for Optimism's Supernode: https://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 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. 19:02:28 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 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 , 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. 19:02:34 One example I can share is the Dafny model we've built for Optimism's Supernode: https://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 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.