This is surprising. SQLite is known for having 100% code coverage, fuzzy testing, and a 644:1 tests to code ratio. If even that cannot stop this kind of attack then we really need to rethink computers from the ground up...
Every little bit helps IMO. Rust seems like it eliminates class of bugs (and so do Haskell and OCaml), the JVM looks like it could prevent another subset of them, and I am sure there are other examples.
Not going to bash anyone for using C -- sqlite's team has their priorities and values clearly stated (performance and discipline) -- but it's probably time for all of us to admit that not all recent tech innovation is about fads. Some of it is actually genuinely useful and helps with age-old problems (though sadly, none of it addresses all of them).
All of them? No. But will a modern language, where many more properties are mathematically proven through the type system, massively improve the situation? Yes.
If you don’t believe me, do the converse and write your next big project completely in assembly (which is effectively untyped), and see what happens.
You currently can bend C++ into ways to have such a type system. The usability this introduced through additional complexity is just very very bad. So no one does it because bad usability means bad productivity and getting a project done with bugs is often better then getting it not done at all (sure there are exceptions!).
That's a good point, and I think you've hit one of the main issues why we're still stuck with old, unsafe languages.
There is the saying that once you got a Haskell program to compile, it usually just works, and I personally found it to be true a lot. But getting it through the compiler can indeed be much more of a journey than in, say, C. And I realize that the work you have to put in to just even being able to run something can be discouraging, maybe going against a natural (or maybe just common) affinity towards tight, iterative "change-compile-try" approaches.
Still, in cases where it really matters, i.e. system software or common, but often mission-critical software like sqlite, maybe it's worth taking the jump?
I would jump with joy if sqlite3 was rewritten in Haskell, OCaml or Rust. They can bring so much to the table in terms of safety and less development surprises.
I am not really talking about the present day, though I agree with the other comments that a lot of modern features help. Think back to the era of Lisp machines. Memory safety, macros, OO... all in the 80s!
We ignored the lessons and paid the price. People, to this day, still look at you weird when you say "I think you could write a game in a garbage collected language" and don't bat an eye when you say "C is dangerous, but I was very careful."
I think what killed us is that computers are expensive (and performance directly translates to the number of computers you need to buy) and security holes are free. Of course you're going to optimize for speed; optimizing for safety can save you at most zero dollars. That's just engineering.
Often times it's more about compatibility with existing libraries or programmers experience then about speed.
I often feel that many very experienced C++ devs have fallen into one of tree fallacies: The sunken (learning) cost fallacy (I include sentimental attachment here). The speed fallacy. And the being totally hypnotised/fascinated by C++-complexity fallacy (I include the you can turn C++ into whatever you like fallacy in this one).
If lockpicking and other ancient hobbies are anything to go on, it doesn't matter how many redesigns you go through; people will just create new specialized/innovative tools to break/attack the most popular ones.
I don't understand this reasoning at all. Locks attempt to artificially limit the (physical) attack surface as well. This could, in fact, be a reasonable definition of a lock. So people come up with wonderful and surprising configurations of matter that cause these artificial limitations to fail providing direct access to the lock's root mechanism (via unanticipated route).
This is analogous to virtual attacks on information systems which are hardened against familiar routes of ingress and vulnerable to those which are wonderful and surprising.
You can apply formal methods to code that you cannot in physical reality. If I show you the equation “x == y”, you won’t be able to pick 7 and 8 to make the equation true. If I give you a mechanical device that works with beads to answer the same question, you might make it work.
Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia.
But all the bugs talked about here are entirely the fault of the software.
Well one could try to change the meaning of "==" to make the equation true. Think about comparator overloading in supported languages where the x and/or y variables are actually objects, for example.
Except you can artificially alter the value of x or y via numerous different methods of attack via frameworks that supersede the code which has been written the formal methods against.
Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive. In a formally verified program, fuzzing is redundant and useless.
Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds?
Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.
My point is that only works if you’re writing the entire software stack. The moment you rely on someone else’s library, whether it’s to read from a file descriptor, a libc wrapper around an OS SYSCALL or whatever, you’re opening up your program to unexpected behaviour. And that’s not even taking into account the slew of very real software bugs that can be introduced from unexpected hardware behavior. Using formal method might prove your applications logic but it doesn’t prove a buffer overflow bug in a library you’ve used, or the OS you’re running on, or the compiler you’ve used from introducing a bug, nor even the hardware itself.
Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.
> Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive.
Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
> In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds
Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
> it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x)
And it does not matter, since the point of formal verification is to help taking those issues into account.
Pardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.
I don’t know about the GP’s wording, but there is a difference. It is possible for a piece of software to be perfectly secure against software-based attacks, i.e. there‘s no possible data you can send it that will cause it to misbehave. It is not possible for a lock to be perfectly secure against physical attacks; if nothing else, you can always break it with brute force.
Of course, even perfect software is susceptible to physical attacks on the hardware it’s running on, but that’s different.
No, there is no difference. Locks and software implement or abide by control laws. In your analogy, if you give perfect software an input and it behaves as expected, then that is the same as walking up to a locked door, trying to open it and failing. Both systems are susceptible to control bypass.
The point is that for some programs[1], you can prove that all inputs will lead to an output with certain properties. With a physical lock, you cannot.
For physical locks, you cannot even rigorously define the "input".
[1] Not always, unfortunately, if your language is turing complete. You might be able to prove weaker, but still very useful statements, like "no input will cause a point to be dereferenced out of bounds".
Yes, you may prove such a statement about a program. But you will not be able to prove that about the physical system where the program is running (assuming you want to run your program and not just reason about it as a mathematical object). If you need an example, consider Plundervolt.
I am not convinced. If your software is secured with any sort of key then you can break this with brute force also. All other attempts to prevent unauthorized access are applications of varying degrees of obfuscation and indirection, the same as in physical lock design.
Then how do explain privilege escalation attacks other than as a user discovering a path to elevated privileges that was not anticipated by the designers? Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
> other than as a user discovering a path to elevated privileges that was not anticipated by the designers
Most of the time, a barrier to elevated privileges that was not correctly implemented, i.e. a bug, not anything the designer did not anticipate.
> Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
So? Does that mean it's not worth looking at the paths where the attacker does not have physical access of the machine that sits in some data center's secured basement?
> It is possible for a piece of software to be perfectly secure against software-based attacks, i.e. there‘s no possible data you can send it that will cause it to misbehave.
I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations.
A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant).
In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough.
Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.
Thanks, this is for once in this thread, a real caveat in the application formal verification (or rigorous type systems). It's hard, it's not unlimited, and one may have fail to state crucial properties that matter in the first place.
Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.)
SQLite is written in a manner/language which only really affords tests, not proof of correctness. (My point was that it might have been written in a language where many of these exploits would not have been possible without subverting the hardware it's running on, but I see from the other responses that I may have phrased it a bit too obliquely.)
Part of the reason SQLite is so prolific is because of the language used, not in spite of it. It’s enabled people to run SQLite on a broad range of hardware, device types and called from any language that supports native C calls (which is a massive array of languages). And let’s not forget the truly amazing performance you get from SQLite too.
Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project?
Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.
Lockpicking if anything shows how robust you can make locks. That there is a complete difference in ease of attack. But physical locks aren't related to mathematical guarantees. The concept may be similar but their implimentations are entirely different.
You can prove it in your model of the system, but you are limited to the model. If your model of the system is the same as the adversaries' then your security design may work. Of course, the real definition of security is financial. No one cares if your lock can be picked by the 1001th person if the security claim is it takes at least 1000 lockpickers to be sufficiently incentivized.
I'm not talking about "security models", I'm talking about plain correctness of software. Any correctness issue (any "bug") can potentially become a security issue if it's reachable through a privilege boundary. And if exploited correctness issues are not in fact the majority of software security issues, they are at least a massive contributor and the subject of this entire discussion.
Examples are a sorted list that inadvertently becomes unsorted while the rest of the program still assumes ordering, or more simply and classically, a pointer that's pointing out of its assumed bounds.
There is no "security model" to consider on that level, and with respect to lockpicking I just wanted to explain why software engineers have access to wonderful tools and methodologies that designers of physical locks don't.
I took a slightly different understanding from that comment than I think you did.
I took the comment in two parts; the second being a tangential suggestion that security is financial.
The first was more interesting. Taken to be a reply to your claim that x=y+1 implies x>y, it is grounded more in theory. The claim is one grounded in a given model - a prevailing mathematical one - and is undoubetdly correct in that model and in the many of the models we use around us.
That does not, surprisingly, make it true.
There are countless models in which it is false, though it seems unlikely these are useful models.
There are also models which are to a degree isomorphic to the current (standard?) models of fancy. In these may lie a way to subvert the expectation of their version of "x>y when x=y+1"
No, because when you are formally verifying programs, or employing a type system that implicitly does so, you take that overflow and any other "surprising" behavior into account. Verifying that the program either cannot reach such an overflow condition, or otherwise handles it correctly, is exactly the point of formal verification.
It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.)
I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.
Well, if you want something as primitive as adding 1, you can prove that a solid plate of steel can't be picked.
Once you get into moving parts and, even worse, useful moving parts, things get a lot trickier. But if you severely limit your inputs you might be able to get somewhere. Like one of those locks where the mechanism pulls the key completely inside before applying it to the keyway: https://www.youtube.com/watch?v=OLsJDELd4lohttps://www.youtube.com/watch?v=5J2rwawhZWI I'd expect many designs in that class to be immune to most definitions of 'picking'.
But my first thought is: how many programs am I using right now on my laptop, that don't have such test coverage? and... how much (probably) undiscovered holes will they have?
That without count, that we're living in the times of the hardware related bugs.
Yes especially for something fairly complex like an sql engine with views and full text search.
Through then it also seems that many of the newer bugs sl seem to be around more advanced features which sometimes can be disabled on compiler time. (newer=after they integrated fuzzing into their tested)
I wonder if it makes sense for Oses to ship two versions of sqlite one for the small local "trusted" database case and one for the sqlite as file format case which had many features disabled, only allowing the core subset of sqlite.
Through if you provide some "evergreen" software you can anyway just include your own version of sqlite. Potentially statically linked in.
Yes? A huge portion of what a database does is amenable to formal methods.
You can even come up with a reasonable rudimentary formal model of a physical machine/CPU and check against that. Sure, the model of the machine may be wrong in subtle ways, but when you discover that, you fix it and recheck your model of a database against the updated model of a physical machine.
That said... don't use a language with trivially allows for out-of-bounds indexing, etc. (SQLite was started when there were really few other good options, so that's understandable.)
(1) Because SQLite is just a function call whereas PostgreSQL
is a round-trip message to a separate server process, MRigger
was able to run many more test cases per second on SQLite.
(2) We fixed bugs faster in SQLite, allowing MRigger to continue
testing SQLite sooner.
(3) SQLite has much stronger backwards compatibility guarantees
than PostgreSQL. We have to continue to support design errors
made decades ago, whereas PostgreSQL gets to walk away from their
poor design choices with each major release. For this reason,
SQLite is rather more complicated than you might imagine.
(4) Many of the bugs found by MRigger had to do with the innovative
(and controversial) decision by SQLite to use flexible typing rather
than strict, rigid typing. SQLite allows you to put text into an
INT column, for example. PostgreSQL has a more traditional design
that simply does not allow that kind of thing, and hence many of the
bugs found by MRigger are simply not applicable to PostgreSQL.
(5) The PostgreSQL developers are very clever people and write
some of the best software around. When we were developing the
cross-DBMS "sqllogictest" test suite for SQLite
(https://www.sqlite.org/sqllogictest/doc/trunk/about.wiki) we were
able to crash every DBMS we tried it on,
except for PostgreSQL. To this day, when somebody has questions
about whether or not the behavior of SQLite is correct, our
reflexive reply is "What Does PostgreSQL Do?"
> (1) Because SQLite is just a function call whereas PostgreSQL is a round-trip message to a separate server process, MRigger was able to run many more test cases per second on SQLite.
Yea, that made it harder in the past for other test tooling too. IIRC Greg Stark fuzzed our regex library and had to fight against the more complicated interaction due to client / server to make that work. Ended up finding quite a few things...
> (3) SQLite has much stronger backwards compatibility guarantees than PostgreSQL. We have to continue to support design errors made decades ago, whereas PostgreSQL gets to walk away from their poor design choices with each major release. For this reason, SQLite is rather more complicated than you might imagine.
FWIW, we (pg devs) are pretty hesitant to break backward compat. Sure, each release has a few things, but it's usually pretty corner case-y stuff. Check e.g. the list for the upcoming v13:
https://www.postgresql.org/docs/13/release-13.html
There's a lot of significant design errors we're continuing to support just because it'd be too painful to break compat.
> SQLite has much stronger backwards compatibility guarantees than PostgreSQL. We have to continue to support design errors made decades ago
Any plans for SQLite4 that will let you get a fresh start and break backwards compatibility so that you can simplify, correct design flaws, etc.? I saw this[0] so I'm guessing it'll just be SQLite3 for now.
Everyone who has been evangelizing strongly typed safe-by-construction languages (or other lightweight formal methods) has been saying this for like 20 years. If you have a memory corruption bug in your application in 2020 it is 110% your fault for making that possible.
It's not surprising. A hack is still a hack, even you apply industry best practices in testing. There are two major security entry points, and none of them were closed since.
Maybe having a way to architect complexity in a way that preserves the author's intent for input data restriction is one way?
Can code be built such that a sql query input could be declared such that it can only be processed in a control flow that ends up interacting with data on disk and return output? I don't mean things like control flow guard that precompute control flow, but an input oriented control flow whitelist enforced by the processor. Programming languages would declare input and explicitly declare what functions can execute as a result of or against that input. So, ideally, each input declaration would have a precomputed control flow graph, the processor will need to register memory as "input" (like NX/DEP) and the program will need to load the control flow graph with an interrupt that causes the processor to track operation resulting from control flow that interacted with the input in memory that is not accessible to the OS. The technology to do this and make it practical exists today but it did't at the advent of modern computing.
Combined with the correctness fuzzing results by SQLancer [1] where SQLite had 179 issues revealed (vs. 11 in PostgreSQL), I think the 100% coverage is a lot less meaningful than I had thought.
Robustness is not necessarily correctness and if the unit tests are just mirror images of the code, their results may help against regressions but little for correctness.
It's a vanity metric, which will prevent programming errors, such as not checking for null, division by zero.
I've seen so many instances of useless tests which don't actually test properly, but simply walk the lines.
Of course, for sqlite I assume the tests are very decent.
Many code coverage tools tell you just if a line/"statement" or similar had been executed during any test.
But that bit might have many possible variants in which you can execute it. E.g. if you have two if/else blocks in a row there are potentially 4 path of execution (if,if; if,else;else,if;else,else). Only two of them need to be hit to get what corresponds to 100% test coverage in most tools.
If you consider that you likely call functions in that if and else statements which can have further branching and similar you might understand why firstly 100% coverage doesn't say to much and secondly why a "real" 100% Coverage if all possible execution paths is normally infeasible.
(Through by using a more powerful type system combined with proofs around the type system and your usage of it you likely can massively prune the number of paths which need testing reachable, but at this point you probably should go full in with the proofs instead of using tests ;=)
> Combined with the correctness fuzzing results by SQLancer [1] where SQLite had 179 issues revealed (vs. 11 in PostgreSQL), I think the 100% coverage is a lot less meaningful than I had thought.
That's really not a honest view of it, the SQLancer page specifically notes:
> The SQLite3 developers were most responsive and very appreciative of our bug reports. They fixed the bugs we reported at an impressive speed, which is why we concentrated on testing this DBMS.
They don't provide run times, but they're empathetically stating most of their runtime is on SQLite. For instance they only have 5 issues for MariaDB because… they stopped testing it as the devs were not responsive.
The thought I had could maybe better expressed as:
"If even SQLite, with its almost unsurpassed testing, has so many 'issues', then that approach of testing cannot be seen as a strong indicator of correctness."
Which is sort of a truism, but seeing the trend of more and more unit tests instead of also investing in other strategies made me blurt that out.
That said, I will continue to use sqlite without hesitation, the robustness is just soothing in a world of terrible libraries.
I love sqlite but I wish they invested in a strict mode. Although thinking about it that's not really "a strict mode of the existing sqlite3" and it's more likely to be "an entirely different library altogether, with some shared code"...
I am basically after an embedded Potgres I suppose. I really wish sqlite went into that space. Or anyone else, really.
> where SQLite had 179 issues revealed (vs. 11 in PostgreSQL)
While I think the skepticism towards the 100% coverage effectiveness is valid, I'm not sure how to make meaningful conclusions from the number of bugs per product reported by that analysis (the analysis itself is certainly a really good job).
MySQL's bug tracker for example is huge (but I don't imply anything negative). During my last two work days, I've experienced two bugs, one of whom was new and caused a server crash with a SELECT. A couple of months ago I've found another server-crashing SELECT, which was also a new bug. I've filed a number of other bugs in the order of the dozens, over the last years.
There is a significant number of bugs reported in the SQLite fulltext functionality (if I understand "FTS" correctly). I don't see any in the MySQL section, and I'm perplexed, since the MySQL FT implementation is (relatively) poor, and I'd be surprised if an in-depth exam wouldn't find any bug.
Possibly, they've dedicated a significant amount of resources specifically to SQLite, either in terms of time spent testing or time spent tooling specific to it.
Yes, you are right, the results are not comparable between DBMS that we tested. For MySQL, the large number of existing bugs prevented us from going further, and also testing more advanced functionality (like FTS). For SQLite (and DuckDB), bugs were typically fixed within hours, which is why we could comprehensively test them. For SQLite, we also tested three extensions (besides FTS, also R*Tree and DBSTAT).
For DBMS, the authors of the APOLLO system found the following [1]:
"Code coverage is a frequently used feedback mechanism in fuzzing engines [22, 27]. We found that this metric is not particularly useful for fuzzing DBMSs, since the core components of DBMS (e.g., query optimizer) already have high coverage (e.g., >95%) after running tens of queries."
I feel like I just watched the original first presentation of SQL injection - this is that big a deal. (I can't find the link, but the guy who gave that presentation thought it bombed because people started getting up and walking out five minutes into his talk - it turned out they were trying to get to the pay phones first so they could call back to their offices and alert them that the world had just been lit on fire).
If I understand this correctly, you need a malicious sqlite database file, which I don’t think you could create with sqlite itself. Which means, in order to exploit this, you first have to get this malicious database onto their computer. So while this seems serious enough, it may not be time to panic quite yet.
I see. I had thought of that more as a format for applications to store their persistent data than for data interchange. When used for the latter, the danger seems clear enough. (I also just noticed that the original post is half a year old.)
If you're using it for persistent storage, its probably inevitable that a user sends in their copy as part of a bug report and a developer cracks it open.
True but even as a interchange file format sqlite is interesting. Through you probably want some hardened against this types of attacks form of sqlite. Like one which had just a subset of features and sqlsupport.
I don't see the practical attack vector. For every use case I have for SQLite, none of them involve allowing someone to execute arbitrary SQL against one of my databases. We also don't do any loading of databases from untrusted parties. Seems like a hypothetical scenario was invented here that could just as well be applied to any database engine with similar outcomes.
The attack is clever and original. AFAIK, nothing like it
has ever been seen before.
Since this attack came to light, SQLite has added features
so that an application can ensure that views and triggers
do not have side-effects (outside of the database file
itself). And if there are no side-effects
then the attack is basically harmless. Sure, the attacker
can still exfiltrate or corrupt data, but the attacker had
to have write access to the database file in order to carry out
the attack in the first place, so exfiltrating or corrupting
data is not an issue - they could already do that. See a
quick summary at https://sqlite.org/forum/forumpost/8beceed68e
Watched it, but all I'm seeing is queries that require arbitrary access in the first place. If you're using sqlite with prepared statements via another programming language, I'm failing to see how these attacks can be used.
Most of these attacks rely on creation of virtual table. Can that be done using a simple select statement with prepared statements?
This is related to the other top post on HN right now about using SQLite as your application file format, which would conceivably involve sending saved files to others.
Not sure why there are comments on this about SQLite's "correctness" or "testing": these are "works as intended" oversights where you run a query and SQLite does as you asked, except if you give an attacker too much control over the query it gives an unpredicted amount of control over what it lets you do. It's similar to command injection: bash could be 100% fuzzed and covered, but if you pass a string into it unescaped it's still going to let an attacker run code…
Yeah this appears to apply more to things like websql. But not in situations where sqlite is used behind a web service that uses prepared statements and best practices and such. If I'm wrong I'd like to know though.
In the context of the recent discussion[1] about using an SQLite database as an application file format, is there a way to mitigate these problems?
For example, a way to verify that the SQLite database has the exact schema that you expect and doesn't have weird views configured to hijack your normal queries?
A lot of comments on this thread ponder the difference between logical and physical, between software and hardware bugs. There is absolutely no difference. As a kind reminder, computation is a physical process, period. Any proofs of correctness apply only within the confines of the model in which they are proven. To the folks fond of formal verification, methinks Kripke agrees. To the folks presenting hardware bugs as a counterexample, it is not. If you include hardware bugs in your security analysis, and you should, you are merely taking a wider view of the system.
These guys seem like they're just trying to get attention and make a name. I'd say if someone has access to install a pre-corrupted file, code execution is already a given.
>> We created a rogue SQLite database that exploits the software used to open it.
So, here, they are replacing the whole database and then stealing the passwords? I would guess that if a malicious actor has that kind of access to the system, all is lost.
SQLite notably is often used as a file format. For example, for browser cookie storage.
As you can see in the next sentence after your quote,
> Exploring only a few of the possibilities this presents we’ll pwn password stealer backends while they parse credentials files and achieve iOS persistency by replacing its Contacts database…
(The major browsers store passwords in SQLite databases, so password stealers upload those to a backend. iOS makes it hard to run code persistently (if you have a shell once, can you keep it after a reboot), so the Contacts database is a target for persistence.)
119 comments
[ 5.3 ms ] story [ 190 ms ] threadhttps://sqlite.org/testing.html
(sarcasm)
Not going to bash anyone for using C -- sqlite's team has their priorities and values clearly stated (performance and discipline) -- but it's probably time for all of us to admit that not all recent tech innovation is about fads. Some of it is actually genuinely useful and helps with age-old problems (though sadly, none of it addresses all of them).
If you don’t believe me, do the converse and write your next big project completely in assembly (which is effectively untyped), and see what happens.
You currently can bend C++ into ways to have such a type system. The usability this introduced through additional complexity is just very very bad. So no one does it because bad usability means bad productivity and getting a project done with bugs is often better then getting it not done at all (sure there are exceptions!).
There is the saying that once you got a Haskell program to compile, it usually just works, and I personally found it to be true a lot. But getting it through the compiler can indeed be much more of a journey than in, say, C. And I realize that the work you have to put in to just even being able to run something can be discouraging, maybe going against a natural (or maybe just common) affinity towards tight, iterative "change-compile-try" approaches.
Still, in cases where it really matters, i.e. system software or common, but often mission-critical software like sqlite, maybe it's worth taking the jump?
We ignored the lessons and paid the price. People, to this day, still look at you weird when you say "I think you could write a game in a garbage collected language" and don't bat an eye when you say "C is dangerous, but I was very careful."
I think what killed us is that computers are expensive (and performance directly translates to the number of computers you need to buy) and security holes are free. Of course you're going to optimize for speed; optimizing for safety can save you at most zero dollars. That's just engineering.
I often feel that many very experienced C++ devs have fallen into one of tree fallacies: The sunken (learning) cost fallacy (I include sentimental attachment here). The speed fallacy. And the being totally hypnotised/fascinated by C++-complexity fallacy (I include the you can turn C++ into whatever you like fallacy in this one).
If lockpicking and other ancient hobbies are anything to go on, it doesn't matter how many redesigns you go through; people will just create new specialized/innovative tools to break/attack the most popular ones.
Programming languages can artificially limit the attack surface. (Up to hardware exploits which can subvert the processor itself.)
This is analogous to virtual attacks on information systems which are hardened against familiar routes of ingress and vulnerable to those which are wonderful and surprising.
Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia.
But all the bugs talked about here are entirely the fault of the software.
Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds?
Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.
Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.
> Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive.
Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
> it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x)
And it does not matter, since the point of formal verification is to help taking those issues into account.
Of course, even perfect software is susceptible to physical attacks on the hardware it’s running on, but that’s different.
For physical locks, you cannot even rigorously define the "input".
[1] Not always, unfortunately, if your language is turing complete. You might be able to prove weaker, but still very useful statements, like "no input will cause a point to be dereferenced out of bounds".
Most of the time, a barrier to elevated privileges that was not correctly implemented, i.e. a bug, not anything the designer did not anticipate.
> Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
So? Does that mean it's not worth looking at the paths where the attacker does not have physical access of the machine that sits in some data center's secured basement?
I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations.
A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant).
In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough.
Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.
Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.)
The cost may indeed be prohibitive, though.
Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project?
Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.
> Sometimes worse is better and moaning about “what if” is neither constructive[...]
... and yet here we are talking about extremely dangerous and possibly far-reaching vulnerabilities in SQLite.
But there are definitely ways to mathematically prove that parts of a program do what they should, or do not do what they should not.
Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive.
Examples are a sorted list that inadvertently becomes unsorted while the rest of the program still assumes ordering, or more simply and classically, a pointer that's pointing out of its assumed bounds.
There is no "security model" to consider on that level, and with respect to lockpicking I just wanted to explain why software engineers have access to wonderful tools and methodologies that designers of physical locks don't.
I took the comment in two parts; the second being a tangential suggestion that security is financial.
The first was more interesting. Taken to be a reply to your claim that x=y+1 implies x>y, it is grounded more in theory. The claim is one grounded in a given model - a prevailing mathematical one - and is undoubetdly correct in that model and in the many of the models we use around us.
That does not, surprisingly, make it true.
There are countless models in which it is false, though it seems unlikely these are useful models.
There are also models which are to a degree isomorphic to the current (standard?) models of fancy. In these may lie a way to subvert the expectation of their version of "x>y when x=y+1"
Most code doesn't check whether incrementing a variable causes an overflow, so in practice the test you're referring to is still vulnerable.
It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.)
I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.
Once you get into moving parts and, even worse, useful moving parts, things get a lot trickier. But if you severely limit your inputs you might be able to get somewhere. Like one of those locks where the mechanism pulls the key completely inside before applying it to the keyway: https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=5J2rwawhZWI I'd expect many designs in that class to be immune to most definitions of 'picking'.
But the vast majority of security problems don’t usually rely on CPU bugs, do they?
I don’t claim it’s exhaustive in general, but it may well decimate a massively common class of problems, and eliminate some of them entirely.
But my first thought is: how many programs am I using right now on my laptop, that don't have such test coverage? and... how much (probably) undiscovered holes will they have?
That without count, that we're living in the times of the hardware related bugs.
Through then it also seems that many of the newer bugs sl seem to be around more advanced features which sometimes can be disabled on compiler time. (newer=after they integrated fuzzing into their tested)
I wonder if it makes sense for Oses to ship two versions of sqlite one for the small local "trusted" database case and one for the sqlite as file format case which had many features disabled, only allowing the core subset of sqlite.
Through if you provide some "evergreen" software you can anyway just include your own version of sqlite. Potentially statically linked in.
You can even come up with a reasonable rudimentary formal model of a physical machine/CPU and check against that. Sure, the model of the machine may be wrong in subtle ways, but when you discover that, you fix it and recheck your model of a database against the updated model of a physical machine.
That said... don't use a language with trivially allows for out-of-bounds indexing, etc. (SQLite was started when there were really few other good options, so that's understandable.)
(I always thought it's obvious)
(1) Because SQLite is just a function call whereas PostgreSQL is a round-trip message to a separate server process, MRigger was able to run many more test cases per second on SQLite.
(2) We fixed bugs faster in SQLite, allowing MRigger to continue testing SQLite sooner.
(3) SQLite has much stronger backwards compatibility guarantees than PostgreSQL. We have to continue to support design errors made decades ago, whereas PostgreSQL gets to walk away from their poor design choices with each major release. For this reason, SQLite is rather more complicated than you might imagine.
(4) Many of the bugs found by MRigger had to do with the innovative (and controversial) decision by SQLite to use flexible typing rather than strict, rigid typing. SQLite allows you to put text into an INT column, for example. PostgreSQL has a more traditional design that simply does not allow that kind of thing, and hence many of the bugs found by MRigger are simply not applicable to PostgreSQL.
(5) The PostgreSQL developers are very clever people and write some of the best software around. When we were developing the cross-DBMS "sqllogictest" test suite for SQLite (https://www.sqlite.org/sqllogictest/doc/trunk/about.wiki) we were able to crash every DBMS we tried it on, except for PostgreSQL. To this day, when somebody has questions about whether or not the behavior of SQLite is correct, our reflexive reply is "What Does PostgreSQL Do?"
Yea, that made it harder in the past for other test tooling too. IIRC Greg Stark fuzzed our regex library and had to fight against the more complicated interaction due to client / server to make that work. Ended up finding quite a few things...
> (3) SQLite has much stronger backwards compatibility guarantees than PostgreSQL. We have to continue to support design errors made decades ago, whereas PostgreSQL gets to walk away from their poor design choices with each major release. For this reason, SQLite is rather more complicated than you might imagine.
FWIW, we (pg devs) are pretty hesitant to break backward compat. Sure, each release has a few things, but it's usually pretty corner case-y stuff. Check e.g. the list for the upcoming v13: https://www.postgresql.org/docs/13/release-13.html
There's a lot of significant design errors we're continuing to support just because it'd be too painful to break compat.
There's a few user visible one that need explicit options to be enabled, and there's documentation for those, of course.
There's other where there's plenty source code level comments explaining the issues.
And some others that "just" are mentioned in discussions.
I can come up with examples if you're interested.
Any plans for SQLite4 that will let you get a fresh start and break backwards compatibility so that you can simplify, correct design flaws, etc.? I saw this[0] so I'm guessing it'll just be SQLite3 for now.
[0] https://sqlite.org/src4/doc/trunk/www/index.wiki
This is the paper describing both. https://research.checkpoint.com/2019/select-code_execution-f...
Can code be built such that a sql query input could be declared such that it can only be processed in a control flow that ends up interacting with data on disk and return output? I don't mean things like control flow guard that precompute control flow, but an input oriented control flow whitelist enforced by the processor. Programming languages would declare input and explicitly declare what functions can execute as a result of or against that input. So, ideally, each input declaration would have a precomputed control flow graph, the processor will need to register memory as "input" (like NX/DEP) and the program will need to load the control flow graph with an interrupt that causes the processor to track operation resulting from control flow that interacted with the input in memory that is not accessible to the OS. The technology to do this and make it practical exists today but it did't at the advent of modern computing.
Robustness is not necessarily correctness and if the unit tests are just mirror images of the code, their results may help against regressions but little for correctness.
[1]: https://www.manuelrigger.at/dbms-bugs/
It's a vanity metric, which will prevent programming errors, such as not checking for null, division by zero. I've seen so many instances of useless tests which don't actually test properly, but simply walk the lines.
Of course, for sqlite I assume the tests are very decent.
But that bit might have many possible variants in which you can execute it. E.g. if you have two if/else blocks in a row there are potentially 4 path of execution (if,if; if,else;else,if;else,else). Only two of them need to be hit to get what corresponds to 100% test coverage in most tools.
If you consider that you likely call functions in that if and else statements which can have further branching and similar you might understand why firstly 100% coverage doesn't say to much and secondly why a "real" 100% Coverage if all possible execution paths is normally infeasible.
(Through by using a more powerful type system combined with proofs around the type system and your usage of it you likely can massively prune the number of paths which need testing reachable, but at this point you probably should go full in with the proofs instead of using tests ;=)
That's really not a honest view of it, the SQLancer page specifically notes:
> The SQLite3 developers were most responsive and very appreciative of our bug reports. They fixed the bugs we reported at an impressive speed, which is why we concentrated on testing this DBMS.
They don't provide run times, but they're empathetically stating most of their runtime is on SQLite. For instance they only have 5 issues for MariaDB because… they stopped testing it as the devs were not responsive.
The thought I had could maybe better expressed as:
"If even SQLite, with its almost unsurpassed testing, has so many 'issues', then that approach of testing cannot be seen as a strong indicator of correctness."
Which is sort of a truism, but seeing the trend of more and more unit tests instead of also investing in other strategies made me blurt that out.
That said, I will continue to use sqlite without hesitation, the robustness is just soothing in a world of terrible libraries.
We can argue about the weak typing though :P
I am basically after an embedded Potgres I suppose. I really wish sqlite went into that space. Or anyone else, really.
While I think the skepticism towards the 100% coverage effectiveness is valid, I'm not sure how to make meaningful conclusions from the number of bugs per product reported by that analysis (the analysis itself is certainly a really good job).
MySQL's bug tracker for example is huge (but I don't imply anything negative). During my last two work days, I've experienced two bugs, one of whom was new and caused a server crash with a SELECT. A couple of months ago I've found another server-crashing SELECT, which was also a new bug. I've filed a number of other bugs in the order of the dozens, over the last years.
There is a significant number of bugs reported in the SQLite fulltext functionality (if I understand "FTS" correctly). I don't see any in the MySQL section, and I'm perplexed, since the MySQL FT implementation is (relatively) poor, and I'd be surprised if an in-depth exam wouldn't find any bug.
Possibly, they've dedicated a significant amount of resources specifically to SQLite, either in terms of time spent testing or time spent tooling specific to it.
"Code coverage is a frequently used feedback mechanism in fuzzing engines [22, 27]. We found that this metric is not particularly useful for fuzzing DBMSs, since the core components of DBMS (e.g., query optimizer) already have high coverage (e.g., >95%) after running tens of queries."
[1] APOLLO: Automatic Detection and Diagnosis of Performance Regressions in Database Systems http://www.vldb.org/pvldb/vol13/p57-jung.pdf
In this case it's relevant, as untrusted SQLite files would be downloaded and loaded in this context.
The expected tables are replaced by views that execute the arbitrary sql.
Since this attack came to light, SQLite has added features so that an application can ensure that views and triggers do not have side-effects (outside of the database file itself). And if there are no side-effects then the attack is basically harmless. Sure, the attacker can still exfiltrate or corrupt data, but the attacker had to have write access to the database file in order to carry out the attack in the first place, so exfiltrating or corrupting data is not an issue - they could already do that. See a quick summary at https://sqlite.org/forum/forumpost/8beceed68e
Sites like https://sqliteonline.com/ and https://inloop.github.io/sqlite-viewer/ could be perpetually vulnerable if not?
Most of these attacks rely on creation of virtual table. Can that be done using a simple select statement with prepared statements?
For example, a way to verify that the SQLite database has the exact schema that you expect and doesn't have weird views configured to hijack your normal queries?
[1] https://news.ycombinator.com/item?id=23508923
Did PHP7 still use an older version at the time of this talk (late 2019)?
I agree with the speaker that the interface of fts3_tokenizer is mind blowing.
So basically a nothingburger.
These guys seem like they're just trying to get attention and make a name. I'd say if someone has access to install a pre-corrupted file, code execution is already a given.
So, here, they are replacing the whole database and then stealing the passwords? I would guess that if a malicious actor has that kind of access to the system, all is lost.
As you can see in the next sentence after your quote,
> Exploring only a few of the possibilities this presents we’ll pwn password stealer backends while they parse credentials files and achieve iOS persistency by replacing its Contacts database…
(The major browsers store passwords in SQLite databases, so password stealers upload those to a backend. iOS makes it hard to run code persistently (if you have a shell once, can you keep it after a reboot), so the Contacts database is a target for persistence.)