At a very quick look, no evidence is given that the "bugs" found in requests are in fact reachable, i.e. not prevented by construction. And sure enough, the very first one is impossible because of a validating guard[1]: `address_in_network` only gets called after `is_valid_cidr`, which enforces the presence of a slash.
I think we should hold claims about effective static analysis and/or program verification to a higher standard than this.
> the very first one is impossible because of a validating guard[1]: `address_in_network` only gets called after `is_valid_cidr`, which enforces the presence of a slash.
It’s correct to flag this code. The check is performed manually outside of the function in question. If you call the function directly, the bug surfaces.
There is no mention in the function documentation of the validation requirement, making it easy to call incorrectly. Also, if it is required to call the validator before calling this function, then the function could just call it itself.
In short, it’s possible to make this code safe by definition, but instead it relies upon the developer to always make the undocumented right choices every single time it is called. I would expect something more rigorous from verified code.
Most (all?) static analyzers are conservative, and reducing your false positive rate is always a struggle. You should never expect a false positive rate of zero (it’s probably impossible to not have false positives), but you shouldn’t be presenting your false positives as successes either.
Sure, but this one doesn’t pass the sniff test. I’ve written plenty of static analysis tools (including ones that do symbolic execution), and one of the first things you do to ensure that your results are valid is create some model of tainting/reachability. Even an analysis that’s 1-callsite sensitive would have caught this and discarded it as a false positive.
(In case it isn’t clear, I’m saying this is slop that someone whipped up and didn’t even bother to spot check.)
What if you asked your favorite AI agent to produce mathematics at the level of Vladimir Voevodsky, Fields Medal-winning, foundation-shaking work but directed toward something the legendary Nikolaj Bjørner (co-creator of Z3) could actually use?
Well, you'd get this embarrassing mess, apparently.
I think we should hold claims about effective static analysis and/or program verification to a higher standard than this.
[1]: https://github.com/psf/requests/blob/4bd79e397304d46dfccd76f...
It’s correct to flag this code. The check is performed manually outside of the function in question. If you call the function directly, the bug surfaces.
There is no mention in the function documentation of the validation requirement, making it easy to call incorrectly. Also, if it is required to call the validator before calling this function, then the function could just call it itself.
In short, it’s possible to make this code safe by definition, but instead it relies upon the developer to always make the undocumented right choices every single time it is called. I would expect something more rigorous from verified code.
(In case it isn’t clear, I’m saying this is slop that someone whipped up and didn’t even bother to spot check.)
Well, you'd get this embarrassing mess, apparently.