5 ms·

I think most of us agree that SQLite is close to the gold standard for stability and testing. This post reminds us that even SQLite has critical bugs. But l

I think most of us agree that SQLite is close to the gold standard for stability and testing. This post reminds us that even SQLite has critical bugs. But looking at https://www.sqlite.org/cgi/src/rptview?rn=7 https://www.sqlite.org/cgi/src/rptview?rn=7 I see a few Core Crash Bugs every month (April has 7). Most of them are not 'critical', to be clear, plenty of 'severe' and 'important' in the list. I don't want to disparage SQLite. They have a free, fantastic product, go to great lengths to have stability no matter what, and document their processes. I learned a lot of them. But clearly, our gold standard is not perfect. So now what? * We might turn to theorem proving. But is it possible at SQLite scale? Are the proofs themselves enough? I remember about a critical piece of software with a proof no incorrect answers would come out. Turns out they forgot to prove the program would end, so they got no answer ever instead of an incorrect one. How do you prove your proofs are complete enough? * We might turn to fuzzing, code analyses, linting,... SQLite does all of them. * Or simply admit we are human, fallible, and try to do the best we can while knowing our limits? Sounds defeatist.

ainar-g 8y ago
I recall reading somewhere that the code of SQLite also has some UB. Which makes me wonder, if they use runtime sanitizers, like ASan, UBSan, etc.
- hyperman1 8y ago
  Might be this: https://blog.regehr.org/archives/1292 https://blog.regehr.org/archives/1292 Looks like SQLite used the sanitizers, and a new tool still found plenty UB. I believe the SQLite auther verified the compiler output for the UB found, and saw it had no impact in practice, so there was no critical bug yet. Then he fixed the UB anyhow. Last paragraph was from vague memories, not from the article, BTW. I would welcome better links.
selckin 8y ago
Or that the basic building blocks/foundations are just terrible
- laumars 8y ago
  I think you're referencing very specific type of bugs while overlooking a whole plethora of other ways a program might fail to follow expectations. As long as we need expressively languages, it will be possible to write bugs (be that low level languages or even "scripting" languages). And as long as we have a diverse ecosystem of hardware and software stacks (and I hope we do continue to) then there will be bugs. Bugs are unavoidable. The point of testing frameworks / fuzzing / etc is to reduce the number and severity of bugs. However if you do have a method of writing 100% bug free code then I'd be interesting in you sharing it ;)
Jweb_Guru 8y ago
> I remember about a critical piece of software with a proof no incorrect answers would come out. Turns out they forgot to prove the program would end, so they got no answer ever instead of an incorrect one. This particular kind of problem is fortunately pretty well-known, though I won't pretend that it's not still a possibility with a lot of proof systems. In the case of SQL databases, we are fortunate in that the base language doesn't provide any mechanism for nontermination (besides WITH RECURSIVE, which most queries will not have). So we don't actually need to prove termination for most queries, but instead provide a proof of "termination-preserving refinment"--that given a query that was already going to terminate (or not), our optimized query will have the same termination behavior (as well as, if it terminates, providing "the same" results, up to the usual SQL caveats about row ordering). Now we'll still have nontermination, but only for queries that are inherently nonterminating (i.e. incorrectly written WITH RECURSIVE queries). As far as "is this kind of proof possible at the SQLite scale": I think it is. The thing it's solving is the sort of thing that is at least reasonably specifiable ("given this SQL query and this data set, these are legal results" and "given these transactions, this is the effect on the permanent storage system"). It would be a huge effort (probably on par with CompCert at a minimum, but I'd bet on significantly more work), but I think it would be worth it: embedded databases like SQLite are very easy to drop into other programs and are used extensively, and one that was formally verified would probably be able to have immediate impact (by comparison, Sel4 or CompCert often aren't in a position to replace existing parts of consumer toolchains). I also think the database is in a position where many people would probably be prepared to sacrifice some of the hardest-to-prove optimizations in exchange for correctness guarantees.
_dps 8y ago
In what other field of substantial complexity is there any expectation that errors never occur? I don't think it's defeatist to accept that there will always be problems. It seems to me in any complex field (medicine, aviation, finance, etc.) the thing that maximizes human success is to design processes so that problems are exposed, treated, contained, and prevented from re-occurring as easily as possible. Looking for something shaped like "problems will cease to exist" seems like a distraction to me.
- bsaul 8y ago
  Software is different than any other field because it's supposed to stand on pure logic. Errors due to hardware failing because of physical properties are expected and unavoidable, but a logical statement no matter how big is supposed to be provable to be correct (except maybe weird self referencing statements, but that's another topic). I think that's what makes our expectations higher in that field as opposed to any other ones.
- waivek 8y ago
  Mathematics
  - kzrdude 8y ago
    If that's true to some extent, is it because Mathematics is built much more slowly, with higher standards of "inclusion" of new elements? Not the same pressure to deliver.
- TickleSteve 8y ago
  'Algorithms' can be proved, 'implementations' necessarily need tests. Algorithms, are mathematically able to be proved, but any real implementation has to involve physical hardware at some level, these implementation details cannot (reasonably) be proven mathematically therefore need sufficient tests. In the absence of a proof, tests can cover both algorithms & implementations.
jonathanstrange 8y ago
> * Or simply admit we are human, fallible, and try to do the best we can while knowing our limits? Sounds defeatist. * That doesn't sound defeatist to me at all, just realistic, as long as it isn't used as an excuse. After all, Sqlite is one of the best tested libraries available.
laumars 8y ago
It's impossible to write bug free code. All these tools we have do is mitigate the number and severity of bugs around. If the remaining ones are weird edge cases that don't affect many people then that's a net win for everyone else. But we shouldn't assume that even "gold standards" are bug free > Or simply admit we are human, fallible, and try to do the best we can while knowing our limits? Sounds defeatist. Not all bugs are manmade (though obviously the vast majority are). But to give examples of other types of bugs: there could be bugs created by compiler optimisations or bugs due to esoteric hardware. Or even features that was intended behaviour but the landscape has since shifted in ways the developers were not aware (I guess you could argue that last point is manmade bit it's arguably not the failure of the developer).
- anfilt 8y ago
  It's not impossible to write, but just extremely hard for anything that is not trivial. For example take function that takes a byte as an input and has byte as an output. Moreover has no external or internal state. You can run through all 256 inputs and check the outputs. However, if the function has 128 bits of input. You could not possibly enumerate all possible inputs and check the output. So it takes other methods to prove it's bug free. This can be hard to find, and there is no way to automate this in all cases. (Halting problem) However, bug free code is not impossible to write. I might say a bug free system is more likely to be impossible since would involve perfect hardware that is also immune to interference, and the physical world can cause a bit to flip while performing a computation.
  - laumars 8y ago
    That code doesn't run independently. You need a compiler, compilers aren't bug free. You need other functions to gain it's input and functions to do something with the output - those might all contain bugs. Even if you're not targeting different OS's or even "POSIX's", and even if you're not targeting different CPU architectures, you still get subtle variations in AMD64 chips that can - if you're working low level enough - throw up some bugs. And if you're not working that low level then you have the entire runtime stack and their bugs to contend with. If computing was still just flipping switches and waiting for LEDs to flash then you might have a point. But in real terms, it's just not possible to write 100% bug free code anymore. The real trick is eliminating all the bugs that people are likely to experience in normal operation and all the bugs that attackers might exploit. Even that is no small feat.
azeirah 8y ago
I don't know.. but isn't time just the thing we need? The more a library gets used, the more bugs that get discovered. So the bugs get reported, fixed and the test-set grows, and the software grows more stable? If the api-surface area doesn't change too much, given the right practices, the software should only grow more stable, right? If bugs like these become rarer and rarer over time, then it's fine, no?
- bsaul 8y ago
  Seems that the bug was introduced in 2016 due to an optimization in ORDERY BY clause. Code that doesn't have to evolve at all for years is very very rare, especially in a product that's used on evolving hardware and software architecture. Responding to parent post, i don't see another solution than theorem provers if we want to pretend that we're doing anything reliable. But it's going to be a long long way...
tzs 8y ago
> We might turn to theorem proving Question: what typically happens when you attempt to prove a program that is not correct, especially a large program? 1. You come to a point where to proceed with the proof you have to show some particular thing, and it is apparent that you cannot show that. The nature of this snag does tell you what to change in the program in order to clear this block. I.e., the proof attempt finds actionable bugs in the program. 2. You come to such a point, but the nature of the snag doesn't tell you anything about why it happened or how to fix it. All you learn is that your techniques are insufficient to resolve the status of this program. 3. You reach a point where you have deduced all that you can deduce and made all the inferences that you can make, but that was not enough to prove the program correct. You haven't hit any particular concrete blocker though. You have simply run out of ideas. Maybe someone else can do better. Question 2: when you have proven some program correct, how hard is it to adapt or update the proof when new features are added to the program? If it takes a lot of work up update proofs, they may only be feasible for programs where the proved version can stay in service for a long time. For programs where a given version can stay in service for a long time, I think we probably should be making more effort to prove them if they are used in areas of importance. SQLite probably does fall into that category for most of its users and use cases.
bvinc 8y ago
I think you have to give up on the idea that you can fix ALL bugs all the time. But I don't think we need to be defeatist. Each layer of tests is an improvement. The benefits of unit testing, integration testing, comparison testing, and fuzz testing are pretty unambiguous. We can always add more layers that give us high assurances against certain classes of bugs. Do we have systems to write programs that are free of dangling pointers? Yes. Double frees? Yes. Buffer overflows? Yes. Seg faults? Yes. With regard to infinite loops, we cannot prove programs in general terminate or not, but we CAN prove that some programs terminate. If our program cannot be proven, we can adjust it until it can. I guess this is similar to theorem proving. We have to be able to define what kind of bug we're talking about, and develop in a system that allows us to prove to ourselves that we no longer have that class of bug. When I talk about a "system", I don't care what it is. Maybe it's a library or set of functions or API that doesn't allow for certain types of errors. Maybe it's a static analysis tool. Maybe it's a language. It doesn't matter, as long as you can have high assurances later that your large code base no longer contains a particular class of errors. Does this get rid of all bugs? No, but it greatly reduces the possible ways that bugs can exist, and that's huge progress.
ksec 8y ago
>I think most of us agree that SQLite is close to the gold standard for stability and testing. One reason I really like DB that are basically thin layers on top of SQLite, like bedrock [1] and some other I cant remember on top of my head. May be one day we see the expanded role of SQLite. [1] http://bedrockdb.com http://bedrockdb.com

ainar-g 8y ago

I recall reading somewhere that the code of SQLite also has some UB. Which makes me wonder, if they use runtime sanitizers, like ASan, UBSan, etc.

hyperman1 8y ago
Might be this: https://blog.regehr.org/archives/1292 https://blog.regehr.org/archives/1292 Looks like SQLite used the sanitizers, and a new tool still found plenty UB. I believe the SQLite auther verified the compiler output for the UB found, and saw it had no impact in practice, so there was no critical bug yet. Then he fixed the UB anyhow. Last paragraph was from vague memories, not from the article, BTW. I would welcome better links.

selckin 8y ago

Or that the basic building blocks/foundations are just terrible

laumars 8y ago
I think you're referencing very specific type of bugs while overlooking a whole plethora of other ways a program might fail to follow expectations. As long as we need expressively languages, it will be possible to write bugs (be that low level languages or even "scripting" languages). And as long as we have a diverse ecosystem of hardware and software stacks (and I hope we do continue to) then there will be bugs. Bugs are unavoidable. The point of testing frameworks / fuzzing / etc is to reduce the number and severity of bugs. However if you do have a method of writing 100% bug free code then I'd be interesting in you sharing it ;)

Jweb_Guru 8y ago

> I remember about a critical piece of software with a proof no incorrect answers would come out. Turns out they forgot to prove the program would end, so they got no answer ever instead of an incorrect one. This particular kind of problem is fortunately pretty well-known, though I won't pretend that it's not still a possibility with a lot of proof systems. In the case of SQL databases, we are fortunate in that the base language doesn't provide any mechanism for nontermination (besides WITH RECURSIVE, which most queries will not have). So we don't actually need to prove termination for most queries, but instead provide a proof of "termination-preserving refinment"--that given a query that was already going to terminate (or not), our optimized query will have the same termination behavior (as well as, if it terminates, providing "the same" results, up to the usual SQL caveats about row ordering). Now we'll still have nontermination, but only for queries that are inherently nonterminating (i.e. incorrectly written WITH RECURSIVE queries). As far as "is this kind of proof possible at the SQLite scale": I think it is. The thing it's solving is the sort of thing that is at least reasonably specifiable ("given this SQL query and this data set, these are legal results" and "given these transactions, this is the effect on the permanent storage system"). It would be a huge effort (probably on par with CompCert at a minimum, but I'd bet on significantly more work), but I think it would be worth it: embedded databases like SQLite are very easy to drop into other programs and are used extensively, and one that was formally verified would probably be able to have immediate impact (by comparison, Sel4 or CompCert often aren't in a position to replace existing parts of consumer toolchains). I also think the database is in a position where many people would probably be prepared to sacrifice some of the hardest-to-prove optimizations in exchange for correctness guarantees.

_dps 8y ago

In what other field of substantial complexity is there any expectation that errors never occur? I don't think it's defeatist to accept that there will always be problems. It seems to me in any complex field (medicine, aviation, finance, etc.) the thing that maximizes human success is to design processes so that problems are exposed, treated, contained, and prevented from re-occurring as easily as possible. Looking for something shaped like "problems will cease to exist" seems like a distraction to me.

bsaul 8y ago
Software is different than any other field because it's supposed to stand on pure logic. Errors due to hardware failing because of physical properties are expected and unavoidable, but a logical statement no matter how big is supposed to be provable to be correct (except maybe weird self referencing statements, but that's another topic). I think that's what makes our expectations higher in that field as opposed to any other ones.
waivek 8y ago
Mathematics
- kzrdude 8y ago
  If that's true to some extent, is it because Mathematics is built much more slowly, with higher standards of "inclusion" of new elements? Not the same pressure to deliver.
TickleSteve 8y ago
'Algorithms' can be proved, 'implementations' necessarily need tests. Algorithms, are mathematically able to be proved, but any real implementation has to involve physical hardware at some level, these implementation details cannot (reasonably) be proven mathematically therefore need sufficient tests. In the absence of a proof, tests can cover both algorithms & implementations.

jonathanstrange 8y ago

> * Or simply admit we are human, fallible, and try to do the best we can while knowing our limits? Sounds defeatist. * That doesn't sound defeatist to me at all, just realistic, as long as it isn't used as an excuse. After all, Sqlite is one of the best tested libraries available.

laumars 8y ago

It's impossible to write bug free code. All these tools we have do is mitigate the number and severity of bugs around. If the remaining ones are weird edge cases that don't affect many people then that's a net win for everyone else. But we shouldn't assume that even "gold standards" are bug free > Or simply admit we are human, fallible, and try to do the best we can while knowing our limits? Sounds defeatist. Not all bugs are manmade (though obviously the vast majority are). But to give examples of other types of bugs: there could be bugs created by compiler optimisations or bugs due to esoteric hardware. Or even features that was intended behaviour but the landscape has since shifted in ways the developers were not aware (I guess you could argue that last point is manmade bit it's arguably not the failure of the developer).

anfilt 8y ago
It's not impossible to write, but just extremely hard for anything that is not trivial. For example take function that takes a byte as an input and has byte as an output. Moreover has no external or internal state. You can run through all 256 inputs and check the outputs. However, if the function has 128 bits of input. You could not possibly enumerate all possible inputs and check the output. So it takes other methods to prove it's bug free. This can be hard to find, and there is no way to automate this in all cases. (Halting problem) However, bug free code is not impossible to write. I might say a bug free system is more likely to be impossible since would involve perfect hardware that is also immune to interference, and the physical world can cause a bit to flip while performing a computation.
- laumars 8y ago
  That code doesn't run independently. You need a compiler, compilers aren't bug free. You need other functions to gain it's input and functions to do something with the output - those might all contain bugs. Even if you're not targeting different OS's or even "POSIX's", and even if you're not targeting different CPU architectures, you still get subtle variations in AMD64 chips that can - if you're working low level enough - throw up some bugs. And if you're not working that low level then you have the entire runtime stack and their bugs to contend with. If computing was still just flipping switches and waiting for LEDs to flash then you might have a point. But in real terms, it's just not possible to write 100% bug free code anymore. The real trick is eliminating all the bugs that people are likely to experience in normal operation and all the bugs that attackers might exploit. Even that is no small feat.

azeirah 8y ago

I don't know.. but isn't time just the thing we need? The more a library gets used, the more bugs that get discovered. So the bugs get reported, fixed and the test-set grows, and the software grows more stable? If the api-surface area doesn't change too much, given the right practices, the software should only grow more stable, right? If bugs like these become rarer and rarer over time, then it's fine, no?

bsaul 8y ago
Seems that the bug was introduced in 2016 due to an optimization in ORDERY BY clause. Code that doesn't have to evolve at all for years is very very rare, especially in a product that's used on evolving hardware and software architecture. Responding to parent post, i don't see another solution than theorem provers if we want to pretend that we're doing anything reliable. But it's going to be a long long way...

tzs 8y ago

> We might turn to theorem proving Question: what typically happens when you attempt to prove a program that is not correct, especially a large program? 1. You come to a point where to proceed with the proof you have to show some particular thing, and it is apparent that you cannot show that. The nature of this snag does tell you what to change in the program in order to clear this block. I.e., the proof attempt finds actionable bugs in the program. 2. You come to such a point, but the nature of the snag doesn't tell you anything about why it happened or how to fix it. All you learn is that your techniques are insufficient to resolve the status of this program. 3. You reach a point where you have deduced all that you can deduce and made all the inferences that you can make, but that was not enough to prove the program correct. You haven't hit any particular concrete blocker though. You have simply run out of ideas. Maybe someone else can do better. Question 2: when you have proven some program correct, how hard is it to adapt or update the proof when new features are added to the program? If it takes a lot of work up update proofs, they may only be feasible for programs where the proved version can stay in service for a long time. For programs where a given version can stay in service for a long time, I think we probably should be making more effort to prove them if they are used in areas of importance. SQLite probably does fall into that category for most of its users and use cases.

bvinc 8y ago

I think you have to give up on the idea that you can fix ALL bugs all the time. But I don't think we need to be defeatist. Each layer of tests is an improvement. The benefits of unit testing, integration testing, comparison testing, and fuzz testing are pretty unambiguous. We can always add more layers that give us high assurances against certain classes of bugs. Do we have systems to write programs that are free of dangling pointers? Yes. Double frees? Yes. Buffer overflows? Yes. Seg faults? Yes. With regard to infinite loops, we cannot prove programs in general terminate or not, but we CAN prove that some programs terminate. If our program cannot be proven, we can adjust it until it can. I guess this is similar to theorem proving. We have to be able to define what kind of bug we're talking about, and develop in a system that allows us to prove to ourselves that we no longer have that class of bug. When I talk about a "system", I don't care what it is. Maybe it's a library or set of functions or API that doesn't allow for certain types of errors. Maybe it's a static analysis tool. Maybe it's a language. It doesn't matter, as long as you can have high assurances later that your large code base no longer contains a particular class of errors. Does this get rid of all bugs? No, but it greatly reduces the possible ways that bugs can exist, and that's huge progress.

ksec 8y ago

>I think most of us agree that SQLite is close to the gold standard for stability and testing. One reason I really like DB that are basically thin layers on top of SQLite, like bedrock [1] and some other I cant remember on top of my head. May be one day we see the expanded role of SQLite. [1] http://bedrockdb.com http://bedrockdb.com