8 ms·
15,000 lines of verified cryptography now in Python
- hall0ween 2y agoI'm cryptographically ignorant. What does this mean for python?
- otterley 2y agohttps://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification Provable correctness is important in many different application contexts, especially cryptography. The benefit for Python (and for any other user of the library in question) is fewer bugs and thus greater security assurance. If you look at the original bug that spawned this work (https://github.com/python/cpython/issues/99108 https://github.com/python/cpython/issues/99108), the poster reported: """As evidenced by the recent SHA3 buffer overflow, cryptographic primitives are tricky to implement correctly. There might be issues with memory management, exceeding lengths, incorrect buffer management, or worse, incorrect implementations in corner cases. The HACL* project https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star provides verified implementations of cryptographic primitives. These implementations are mathematically shown to be: memory safe (no buffer overflows, no use-after-free) functionally correct (they always compute the right result) side-channel resistant (the most egregious variants of side-channels, such as memory and timing leaks, are ruled out by construction)."""
- jessekv 2y agoMore context here. https://github.com/python/cpython/issues/99108#issuecomment-1306337205 https://github.com/python/cpython/issues/99108#issuecomment-...
- aseipp 2y agoExtreme ELI5 TL;DR: Your Python programs using the cpython interpreter and its built in cryptographic modules will now be using safer and faster, with no need for you to do anything.
- odo1242 2y agoIs it faster? I’m pretty sure the main goal of this effort is just the “safer” part.
- aseipp 2y agoThe goal is to make things safer, yes, but speed is absolutely a major priority for the project and a requirement for production deployment, because the difference in speed for optimized designs vs naive ones might be an order of magnitude or more. It's quite speedy IME. To be fair to your point, though, it's also a moving target; "which is faster" can change as improvements trickle in. Maybe "shouldn't be much slower" is a better statement, but I was speaking generally :) (You could also make the argument that if previous implementations that were replaced were insecure that their relative performance is ultimately irrelevant, but I'm ignoring that since it hinges on a known unknown.)
- drewcoo 2y agoAnd safer is often slower to avoid timing attacks.
- aseipp 2y agoI mean, most if not all of the code they're replacing (e.g. the vendored and vectorized Blake2 code) is also going to be designed and optimized with timing attacks in mind and implemented to avoid them. CVE-2022-37454 was literally found in a component that was optimized and had timing attack resistance in mind (XKCP from the SHA-3 authors). "Code that is already known to be wrong" is not really a meaningful baseline to compare against.
- protz 2y agothe performance was pretty much identical, however, as an added benefit, Blake2 got quite a bit faster due a combination of 1) our code being slightly more optimized, and 2) python's blake2 integration not actually doing runtime cpu detection, meaning that unless you compiled with -march=native (like, Gentoo), at the time, you were not getting the AVX2 version of Blake2 within Python -- my PR fixed that and added code for CPU autodetection bear in mind that performance is tricky -- see my comment about NEON https://github.com/python/cpython/pull/119316#issuecomment-2181717804 https://github.com/python/cpython/pull/119316#issuecomment-2...
- hathawsh 2y agoHere is how I read it: CPython has a hashlib module that has long been a wrapper around certain functions exported from OpenSSL, but since a SHA3 buffer overflow was discovered in OpenSSL, the CPython project has now decided to wrap a library called HACL*, which uses formal verification to ensure there are no buffer overflows and other similar bugs.
- thebeardisred 2y agoLines of code is a pretty poor measurement. Doubly so when you're boasting a large number in the context of cryptographic code.
- daquisu 2y agoWhich better measurement do you propose?
- bbstats 2y agothe 2nd sentence: "As of last week, this issue is now closed, and every single hash and HMAC algorithm exposed by default in Python is now provided by HACL*, the verified cryptographic library." it's describing coverage.
- bbeonx 2y agoThis isn't really a metric. It's a description to help the reader understand the magnitude of effort that went into this project. SLoC is a bad metric for plenty of things, but I think it's fine for quickly conveying the scope of a project to a blog reader.
- evertyhingisfin 2y ago[flagged]
- Tarucho 2y agoNot saying it isn´t useful but with this change Python's crypto depends on Microsoft (https://fstar-lang.org/ https://fstar-lang.org/ and https://project-everest.github.io/ https://project-everest.github.io/)
- NavinF 2y ago> HACL* is a formally verified library of modern cryptographic algorithms, where each primitive is verified for memory safety, functional correctness, and secret independence. HACL* provides efficient, readable, standalone C code for each algorithm that can be easily integrated into any C project. > All the code in this repository is released under an Apache 2.0 license. The generated C code from HACL* is also released under an MIT license. You have an unusual definition of "depends on Microsoft". Anyone worried about depending on Microsoft should be able to maintain 15k lines of C that are already formally verified. Python already vendored the code so who cares who wrote that code?
- Tarucho 2y ago[flagged]
- IlikeKitties 2y agoModern, ubiquitous cryptography is now practically unbreakable (even for the NSA) and widely used. The crypto wars of the 90s seem rather quaint. Any thoughts on the effects on society this now has?
- xyzzy123 2y agoIt's cool that we can largely "strike out" link level wiretapping from our threat models but it just means attackers move on to the endpoints. I have a wonderfully private link to google, my bank and my crypto exchange but all of those are coerced to report everything I do.
- TacticalCoder 2y ago> ... but it just means attackers move on to the endpoints. Yup but this doesn't scale anywhere near as well for the attackers.
- pyfon 2y agoExcept for countries who hist companies who hold all the endpoints.
- artursapek 2y agoMost internet traffic is cosolidated through a small number of providers like Cloudflare and AWS.
- hkt 2y agoCloudflare being, if it wants to be, an epic MITM given its control of DNS and its role as WAF. Line level surveillance barely matters now.
- FabHK 2y agoSorry, if there are N clients, and M servers, then there are N+M endpoints, but N*M links, which is a lot more.
- Retr0id 2y agoWill this bring support for "streaming" output from SHAKE? Here's the (recently closed!) issue for pyca/cryptography regarding this feature, although I can't find an equivalent issue for the python stdlib: https://github.com/pyca/cryptography/issues/9185 https://github.com/pyca/cryptography/issues/9185 Edit: Found a relevant issue, "closed as not planned": https://github.com/python/cpython/issues/82198 https://github.com/python/cpython/issues/82198
- tsecurity 2y agoHow much of the development of this was verified, and what does that consist of? I worry a little when I read that things are verified and were hard.
- rtkwe 2y agoThe first two shouldn't matter because the entirety of the code is verified and anyone can check the verification. The last is an issue with any cryptography but verification doesn't try to address that only that the code does precisely and only what it's supposed to; ie it should guarantee that there are no exploits possible against that library.
- aseipp 2y agohttps://eprint.iacr.org/2017/536.pdf https://eprint.iacr.org/2017/536.pdf is the relevant paper that introduces the project and its broad design. Figure 1 on page 3 is a good place to look.
- bgwalter 2y agoReading the article, they took a verified C library generated from F* from Microsoft, vendored the code in CPython and wrote a C extension. And during the process they discovered that the original library did not handle allocation failures? What is the big deal about Python here? It's just another wrapped C library.
- anon6362 2y agoIn general, it's good practice to use best components available, regardless of source. Cryptographic components especially shouldn't be DIY. It would be cool if Ruby did something similar for stdlib/openssl, but it could be also be done in a gem too.
- quantumgarbage 2y agoA seamless, drop-in replacement, for all python users is actually a pretty good feat tbh
- nine_k 2y ago> just another wrapped C library. I suppose you mean "just another top-notch library available in the Python ecosystem"? :)
- bolognafairy 2y agoWhat part of how this is being conveyed do you disagree with? Specifically. This isn’t a language war.
- neuroelectron 2y agoThe headline makes it sound like it was written in Python which is a lot more readable than 15,000 lines of C
- frumplestlatz 2y agoThe 15k lines of C are generated. The implementations are written in (and formally verified using) F*, and then the C is generated from the F* code using KaRaMeL. One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly. - https://fstar-lang.org https://fstar-lang.org - https://github.com/FStarLang/karamel https://github.com/FStarLang/karamel - https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star
- chrisrodrigue 2y agoThere's no mention of what Python version this is actually in. After some digging, it looks like the answer is 3.14 [0], so we won't be seeing this until October [1]. One could argue that this is a security fix (just read the first sentence of the blog post) and should be included in all the currently supported versions (>=3.9) of Python [2]. [0] https://github.com/python/cpython/blob/main/Doc/whatsnew/3.14.rst#hmac https://github.com/python/cpython/blob/main/Doc/whatsnew/3.1... [1] https://peps.python.org/pep-0745/ https://peps.python.org/pep-0745/ [2] https://devguide.python.org/versions/ https://devguide.python.org/versions/
- ashishb 2y agoMany famous libraries like Spacy do not support Python 3.13 and are stuck on Python 3.12 (Oct 2023). So, even if this comes out in Python 3.14, any non-trivial project will have to wait till Oct 2026 (or Oct 2027) to be able to use it. 1 - https://github.com/explosion/spaCy/issues/13658 https://github.com/explosion/spaCy/issues/13658
- pbronez 2y agoJust ran into something similar with Great Expectations. Python 3.12 is the newest I can run.
- 0cf8612b2e1e 2y agouv seems to have reverted to defaulting to 3.12 instead of 3.13. Which I fully endorse owing to how many packages are not yet compatible.
- ashishb 2y agoExactly, many compiled languages like Java and Go do not suffer from this issue.
- fiddlerwoaroof 2y agoTell that to all the companies stuck on Java 8 with old versions of Spring and Hibernate. This is the cost of an ecosystem where major libraries make breaking changes.
- pluto_modadic 2y agodoes this mean anything that imports the cryptography modules needs to include G++ or something weird, or is it compiled into cpython itself?
- __s 2y agoThe latter. Most of CPython is C you don't need compiler to run
- badmonster 2y agohow reusable is the generic streaming verification framework beyond cryptographic hashes?
- AndyMcConachie 2y agoThank you!
- jart 2y agoI think it was pretty obvious to anyone who looked at the SHA3 code Python had that it was insane and not to be trusted. Everyone smart moved on to blake2b. How they managed to frameworkify a hash function and push it through standardization, I'll never know.
- Surac 2y agoThis all reads like if any new version of python breaks old stuff? Never thought python is unstable
- procaryote 2y agoMinor versions of python knowingly break things all the time, often to remove something that was earlier deprecated because a tidy namespace is more important than backwards compatibility, apparently. The fact that you often won't find out until runtime makes it a real pain It's a mess.
- sylware 2y agoAnd who in going to "verify" the machine code produced by the compiler used for the python interpreter itself? (then the hardware would have to be validated as well if complex ISA). The point is, cryptography should be mostly if not all assembly. Look at dav1d AV1 decoder to have an idea.
- andai 2y agoMy first thought was "in the Python language", but it's a C extension. Is it even possible to write crypto code in memory managed languages? Due to the need for everything to run in constant time.
- martinky24 2y agoIIRC Go has pretty decent crypto implemented in Go: https://pkg.go.dev/crypto https://pkg.go.dev/crypto
- EasyMark 2y agorust is a type of memory managed language and I don't see any issue with writing crypto there?
- dymk 2y agoc++ is a (poorly) memory managed language by that logic (std::unique_ptr, etc)
- EasyMark 2y agoActually c++ is also excellent if you use modern c++20 and greater. Crypto algos tend to be fairly small compared to a lot of other software and if you can't keep your coders disciplined enough to use memory safe code there then the company or project should probably go under because of skills issues.
- dymk 2y agoAlright, enjoy your RCEs. I’ll be over here being productive, despite my skill issue.
- wolf550e 2y agoPlenty of cryptography in Java, C# and Go.