xavxav

14 ms·

121.
by xavxav 5y ago
It's good that they're making efforts, but in practice it still feels highly lacking: in france there are many competing & overlaping semi-public and public organisations whose copyright stance makes OSS difficult, even when t
122.
by xavxav 5y ago
Sort of hijacking, but I've always wondered: Where are our 'neural binutils'? I want to be able to compose these tools like I would random unix ones: Something like 'Identify album covers in this image | extract the text
123.
by xavxav 5y ago
There are similar approaches, ie: Checked-C which work surprisingly well. However, I'm not sure that this approach would be expressive enough to handle the edge cases of C craziness and pointer arithmetic. There's more to memory u
124.
by xavxav 5y ago
A crash is signficiantly better than corruption. If you can force an `unwrap` you can cause a denial of service but with corruption, all bets are off.
125.
by xavxav 5y ago
Right, but a memory unsafety but is what takes a harmless logic bug in an image parser with no filesystem access to an RCE and sandbox escape. Memory unsafety allows you to change the 'category' of the bug, you become free to do
126.
by xavxav 5y ago
> Honestly at this point I’ve given in and am now advocating that we rewrite every damned widget from scratch in Rust, because by the time we’re mostly done, my career will be winding down, and seeing that shit still gets pwned like, ex
127.
by xavxav 5y ago
Rust is used in production though at large companies: Amazon, Microsoft, Mozilla, etc... I would be highly surprised that the borrowchecker would be the reason code couldn't ship in the first place, once you get over the initial ment
128.
by xavxav 5y ago
Not to go all 'Rust Evangelism Strike Force' but almost universally, these exploits leverage memory unsafety somewhere in the stack, usually in a parser of some kind (image, text, etc). The fact that this is still tolerated in our
129.
by xavxav 5y ago
Yea, I think that they're taking the correct approach. For certification reasons formal verification is not necessary or even really desirable, but a core hypothesis in my thesis is that we can lower the exponential factor of formal me
130.
by xavxav 5y ago
I've talked to Yannick quite a lot in the past as my lab develops Why3 and SPARK uses my translation for their new support for pointers (access types). Additionally, my advisor collaborates with them on counterexample generation, espec
131.
by xavxav 5y ago
I already do, my tool produces WhyML modules from Rust crates. But we can leverage Rust's ownership typing to drastically reduce proof obligations related to pointers and memory. Incidentally, I've started working on a VSCode fr
132.
by xavxav 5y ago
That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.
133.
by xavxav 5y ago
That’s my long term plan, I’d like to build something like Frama-C ( https://frama-c.com/ ) but for Rust, but verification tools are not like other development processes and it’s not easy to piece them together. I think that
134.
by xavxav 5y ago
This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated. I'm curious what kinds of software they want to (eventually) verify, my Ph
135.
by xavxav 5y ago
no, it isn't. Don't go around spreading FUD, the article makes no mention of causation for the deaths, extrapolating that to an entirely hypothetical (and unfounded) vaccine induced immunodeficiency is unjustified.
136.
by xavxav 5y ago
GDPR fines can go up to 4% of global revenue so the 62 cent comparison seems apt.