Earlier quoted context omitted.
Nigel has said that emitting "unsafe" Rust is a reasonable thing for a hypothetical WUFFS 1.0 to be able to do as an alternative to C. As with good "unsafe" Rust written by humans WUFFS would know exactly why what it's doing is fine, it's just that the Rust compiler can't necessarily see that, hence the need to label it "unsafe". Today C makes most sense given the WUFFS language is still in flux. [Edited to fix a ser…
What would be the primary benefit of emitting Rust rather than C? Both would be considered safe (assuming Wuffs generates correct code), and Rust could access the C code via FFI. Is there something I’m missing?
Wuffs: Wrangling Untrusted File Formats Safely
51–60 of 73 posts
Re: Wuffs: Wrangling Untrusted File Formats Safely
#52Earlier quoted context omitted.
What would be the primary benefit of emitting Rust rather than C? Both would be considered safe (assuming Wuffs generates correct code), and Rust could access the C code via FFI. Is there something I’m missing?
One benefit would be that Rust users could use Wuffs code without having to install a C compiler. Pure-Rust solutions are much more convenient in the Cargo ecosystem than wrangling -sys crates.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#53Earlier quoted context omitted.
Nigel has said that emitting "unsafe" Rust is a reasonable thing for a hypothetical WUFFS 1.0 to be able to do as an alternative to C. As with good "unsafe" Rust written by humans WUFFS would know exactly why what it's doing is fine, it's just that the Rust compiler can't necessarily see that, hence the need to label it "unsafe". Today C makes most sense given the WUFFS language is still in flux. [Edited to fix a ser…
What would be the primary benefit of emitting Rust rather than C? Both would be considered safe (assuming Wuffs generates correct code), and Rust could access the C code via FFI. Is there something I’m missing?
Re: Wuffs: Wrangling Untrusted File Formats Safely
#54Earlier quoted context omitted.
WUFFS is provably safe - that's the whole schtick. If a WUFFS kernel exists, you can assume it is safe. If it's not proven safe, it doesn't compile. The reason everyone doesn't program in WUFFS is that you have to write a proof that your kernel is safe, which takes a very very very long time.
What's the formal verification story for WUFFS?
The clever idea is to have you the programmer in effect write a proof that your code has the desired semantic properties as part of the programming activity and so then the WUFFS transpiler is merely checking that the proof is correct.
This leverages your understanding of what you were trying to do.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#55Earlier quoted context omitted.
Wait, you believe that somehow one of these approaches doesn't rely on competence from programmers? How do you figure? Have you been imagining that sandboxes are some sort of fairy dust we just stumbled onto one day, supernatural in nature and not, in fact, just software written by people you're hoping are competent and haven't left any holes?
The point was... one is testing parser/OS integrity via a debugging interface over an expectation of an unchanging emulated environment state... there is nothing particularly special about the approach. Even Qubes OS and RancherVM is not perfect in this regard friend. Or put another way, the available attack surface of a bare-minimum fixed environment is much easier to auto-audit, than a pile of daily permuted binari…
If you're Matt Godbolt the benefits of sandboxing outweigh the cost because Matt is interested in general purpose software. But WUFFS isn't for that, as its name says it's interested in doing one particular task well.
In this deliberately limited domain, WUFFS gets to sidestep Rice's theorem altogether and just prove the software meets the semantic requirements [technically you do the proving, WUFFS just checks your work].
I hope you enjoyed your goldfish crackers but I urge you to use the right tool for the job.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#56Does anyone know of a tool that can do this for PDFs instead?
pdfs are really really hard. the only viewer that parses them semi-correctly is ... Acrobat Reader. try to ever read any code for PDFs and see all the horrors. Google gave up and just bought the code from foxit.
They just bought foxit code to save years of development when they wanted to ship PDF reader in Chrome.
Your comment about "the only viewer that is semi-correct" is also wildly off the mark.
Parsing correctly written PDF files is hard but multiple engines can do it correctly.
Parsing real life PDFs is much harder then correctly implementing PDF spec because lots of PDFs are just broken. They generators create invalid PDF files and then PDF readers have to spend heroic efforts to somehow make sense of this brokenness. Adobe does it better than most because... well it would be embarrassing if they didn't. They invented the format, they make money from their tools, they were doing it the longest, they have the largest archive of broken PDFs for testing etc. It's hard to expect that e.g. an open-source project with one or two developers can match that.
I work on SumatraPDF so I know.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#57Earlier quoted context omitted.
The point was... one is testing parser/OS integrity via a debugging interface over an expectation of an unchanging emulated environment state... there is nothing particularly special about the approach. Even Qubes OS and RancherVM is not perfect in this regard friend. Or put another way, the available attack surface of a bare-minimum fixed environment is much easier to auto-audit, than a pile of daily permuted binari…
There's nothing special about it, but it doesn't work especially well. This is the strategy that's blown up on Apple twice in recent years and will keep burning them. If you're Matt Godbolt the benefits of sandboxing outweigh the cost because Matt is interested in general purpose software. But WUFFS isn't for that, as its name says it's interested in doing one particular task well. In this deliberately limited domain…
The design in question currently only processes around 1.8M large image files a day, and does not require additional work/re-implementations to support the dozens of questionable user file-formats. i.e. the plain old ImageMagick lib does most of the heavy lifting at the end.
Would I trust such a solution for something like a native client side web-browser etc... absolutely not... but for the core-bound instance overhead, the resource cost was acceptable for almost a decade of uptime on those system instances.
Use-cases are funny like that, as there is no perfect solution... but rather a tradeoff of what features get the system functional and reliable. Part of that is admitting integration of 3rd party dependencies is a long-term liability, and domain specific languages almost always fade into obscurity.
Cheers, =3
Re: Wuffs: Wrangling Untrusted File Formats Safely
#58Can Wuffs provide stronger safety guarantees than techniques like WasmBoxC? My understanding is that compiling unsafe C to WASM and back would also guarantee safety with respect to buffer overflows, integer arithmetic overflows and null pointer dereferences. It’s nice not annotating code to explicitly prove invariants to the compiler like you would in say Wuffs or Rust, but I suppose that’s what limits performance.
Not fatal, but perhaps annoying.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#59Wuffs is great. I use it in Substrata ( https://substrata.info/ ) for loading PNGs. It is both faster and safer than LibPNG. It's something around 2x faster than LibPNG in my tests (depending on the PNG file), see timings here: https://github.com/google/wuffs/issues/13#issuecomment-17325... So generally Wuffs is great and you should use it to decode your PNGs. There are some downsides: not all of the obscure bit dept…
My understanding is that libpng is unoptimised and 5-10x faster is possible.
The biggest bottleneck in PNG decoding is zlib, which is not part of libpng. There are faster inflate implementations, but nowhere near 5x.
The second slowest thing is unfiltering, but it takes only 10-20% of the decoding time, so even lightspeed implementation would make little difference.
There is possibility of a 10x difference when encoding, but that's not due to libpng being slow, but because it's possible to apply worse compression and there are dedicated crappy-but-veryfast encoders.
Re: Wuffs: Wrangling Untrusted File Formats Safely
#60This is one of my favorite attempts at better programming language safety, because it compiles down to C that can then be shipped like normal C, so you don't get the ecosystem friction like with ex. Rust.
What's the difference vs compiling down to machine code and linking it with your program?