Hi,

There was a recent post on Hacker News about the extensive test suite for SQLite https://news.ycombinator.com/item?id=46303277

Something I have always wondered is how effective formal verification would be on a database system like SQLite. Given that the test suite is very complete and that the cost of formal verification is going down, it might even be economically relevant.

If done correctly, it would really mean there are no bugs, apart from system outside of SQLite itself (like the C compiler, OS primitives, ...). Optimizations could be more aggressive; for example, this is one of the main reasons AWS claims to use formal methods.

Is that something you have been looking at and think is worth considering?

"Formal methods" is a name grouping many different techniques, from static analysis to full theorem proving. Only the latter would be effective to fully verify a codebase like SQLite.

Formal verification is a technique for ensuring that all bugs in the design specification are faithfully reproduced in the implementation. Formal verification does not prevent bugs. It merely shifts the source of the bugs from the implementation back to the design specification.

Yes, but the "design specification" is much simpler than the code, especially for an optimized C program like SQLite. There, the design specification would be the naive implementation of SQL without caring at all about algorithmic complexity, in a functional language.

There is also a well-tested design specification, which is the current SQLite version, on which further optimizations could be applied while being quite sure nothing is breaking.

I can also quote the CompCert formally verified C compiler, which was the only compiler found without bugs after an extensive fuzzing with GCC, Clang, and other popular compilers, which all got subtle issues.

Yes, but the "design specification" is much simpler than the code, especially for an optimized C program like SQLite.

Mythinks you have never actually tried to write a formal design specification for something like SQLite. It turns out to be rather more complex than you might imagine. I invite you to try it and see for yourself.

I have tried to write a formal design spec for SQLite. I spent years working on it, but it never got anywhere close to being complete. And after all that time and effort, I never found it to add any value to the project, so I eventually abandoned the effort.

Maybe you can do better. Maybe you know some tricks for writing formal design specifications that I don't, and that make the process easier. Try it yourself. Prove me wrong.

OK, thanks for your answer, we indeed need to try, we will try!

Hi,

As an update, we made experiments around the formal verification of the SQLite code, using the approach of translation with AI of the C code to the formal language Rocq, generating equivalence tests.

This is only the first step of a full formal verification, which would additionally require proving the equivalence of the translation to the original C code and verifying properties about this translation.

We conclude that this is still a big project to run with current technologies. We still made the translation of a substantial part of the B-tree implementation to Rocq, with corresponding tests. Results are in https://github.com/formal-land/rocq-of-db repository. We added many conventions and tests to make the translation with LLMs more stable, but even with that, it is starting to be too unstable and uses too many tokens, so we are switching to a simpler project.

We are happy to continue working on it when having more availability. Best!

Thank you for feeding back. It's interesting to see where the currently state of such technological tools is - presumably in X years time the answer may be different.

Hi lol thanks for whoever bumped this thread.

i was learning how to use formal methods - not for sqlite but for turso. but since sqlite is our defacto standard and is obviously more reliable and have better docs, i picked sqlite-c-api to try and i agree it takes sooo long but quint(the tool i was using to do this) found a counter example.

for this case

package require sqlite3

file delete -force tcltestingcapi.db tcltestingcapi.db-journal tcltestingcapi.db-wal
sqlite3 db tcltestingcapi.db
db eval {CREATE TABLE t(x); INSERT INTO t VALUES(1),(2);}

set seen 0
set blob [db serialize main]
db eval {SELECT x FROM t} {
  incr seen
  if {$seen == 1} {
    db deserialize main $blob
  }
}

db close

c file repro: https://gist.github.com/Pavan-Nambi/83f04a6f1d189a58adf98bde73257c59

on mac os both are seg fault crashes

on linux... sometimes it crashing sometimes its not and on valgrind it says invalid reads from freed memory, SQLITE_CORRUPT (database disk image is malformed)

i haven't made any report regarding this cuz.. most of the time i am second guessing myself thinking if i am doing something wrong or something i am not allowed to. but seeing this thread pop up gave me little courage..

SQLite docs say sqlite3_deserialize() fails with SQLITE_BUSY if the database is currently in a read transaction

i could push my repo to github - when i get back home in 5-6 hours. if anyone is interested.

sorry i know this message might sound very unclear and all over the place. i am typing from mobile and not near my pc/home, was just excited when i saw this discussion.... again i could very well be doing something wrong/invalid usage. if that's the case please let me know, thanks

Also yes - I could be wrong here, I could be doing something stupid. I'm not expert and still learning things, so I appreciate any feedback, thanks

thanks, this seems to be fixed in trunk now https://github.com/sqlite/sqlite/commit/1fc7341ad2331b31ba5edc0160554ce4a1bef35e

for anyone interested in gh repo here - https://github.com/Pavan-Nambi/sqlite-c-api-quint

please note that there might some inconsistencies - it is part of my formal-methods-learning repo i keep locally i only pushed relevant things so some stuff in there might reference things u don't see on github.

SQLite docs say sqlite3_deserialize() fails with SQLITE_BUSY if the database is currently in a read transaction

Thanks to your post including easy reproductions, this was quickly fixed: src:77662cce9a

my tests are failing on this now...

Please try out src:1f940357f7 and let us know if it's still failing.

hi, thanks, i no longer have any crashes around deserialise, i am trying to add more funcs

as of now this is where it fails:

 sqlite3 src :memory:
  src eval {
    CREATE TABLE t(x);
    INSERT INTO t VALUES(1);
  }
  set blob [src serialize main]

  sqlite3 dst :memory:
  dst deserialize -readonly 1 $blob

  set ro [sqlite3_db_readonly dst main]
  set rc [catch {dst eval {INSERT INTO t VALUES(2)}} msg]

  puts "db_readonly=$ro"
  puts "write_catch_rc=$rc"
  puts "write_msg=$msg"

  Observed:

  db_readonly=0
  write_catch_rc=1
  write_msg=attempt to write a readonly database

in specs i was expecting db_readonly to be 1

sqlite docs say

The sqlite3_db_readonly(D,N) interface returns 1 if the database N of connection D is read-only, 0 if it is read/write, or -1 if N is not the name of a database on connection D.

second issue is: this looks like most recent change..

  for {set i 0} {$i < 200000} {incr i} {
      alloc_dealloc_mutex
    }
    puts DONE

sometimes i am getting undefined behaviour , sometimes no,

sqlite3.c:30828:32: runtime error: member access within misaligned address 0x000106358e90 for type 'sqlite3_mutex' (aka 'struct sqlite3_mutex'), which requires 128 byte alignment
0x000106358e90: note: pointer points here
 00 00 00 00  00 00 00 00 00 00 00 00  00 00 00 00 00 00 00 00  00 00 00 00 00 00 00 00  00 00 00 00
              ^ 
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior sqlite3.c:30828:32

also another issue i just want to ask what's the expected output here.... (i'm likely writing specs wrong to run into this lol) or if this should give api misuse

https://gist.github.com/Pavan-Nambi/e2db9f211d5607876d1caa2c4071ead1

currently this gives

  backup_step rc=0
  deserialize rc=11 (SQLITE_CORRUPT)
  errcode=11 ex=11 msg=malformed database schema (x) - invalid rootpage

sqlite3.c:30828:32:

Without knowing the very specific version you're using, line numbers are not terribly useful. Please always provide a version hash (preferably the one from the canonical source tree rather than github, as that saves us having to back-track the github hash). The simplest way to get that in your case is:

$ grep 'define SQLITE_SOURCE_ID' sqlite3.c

The mutexes were recently re-packed to use 128-byte alignment and you may have discovered a regression involving that.

i'll need to ask Dan or Richard to address your other points.

PS: at this point we have thoroughly threadjacked someone else's largely-unrelated thread. Please post future reports in new threads.

Writing formal specifications isn't easy indeed, but it's the basis for building really proven-correct code.

The root of SQL and how it's supposed to work is already based on mathematics, so this part is not the most complex to express formally (mathematically).

In my experience, the best formal method for "assigning programs to meanings" is the B method. Starting form abstract formal specifications, from there successive steps of refinment (with obligatory proofs) make the model closer and closer to what is aimed at the low level (code) while insuring mathematical correctness at every step. Then a final step is converting the final B model into B0, ready for compiling in Ada, C, C++ by certified compilers. That is production of formally proven-correct programs.

This is the opposite approach of the OP, where one first write C (say) code (with potential bugs), then use tools to convert that into Coq (or its friends), then brainstorm on what are the supposed invariants and specifications meant at that level, etc. That is formal verification.

Hi,

I do get your point and agree it dows not prevent all bugs.

OTOH if you have a fresh approach (a formal specification or another implementation) for any difference you encounter, you can check if one or the other is wrong/a bug. Sometimes this might result in a clarification of some edge cases where the behaviour is currently unspecified, sometimes it will show errors in the fresh approach, sometimes it will discover problems in the current implementation.

Unless someone blindly repeats the same mistakes or blindly faithfully reproduces specification bugs to the shipping software, the odds would be that some bugs would be found/prevented from having an impact.

Regards, ralf

I would argue that the design specification for SQLite is its documentation, available at https://sqlite.org.

Would you like to try formally verifying SQLite from that ? It would take thousands of hours. And do you think you could do a better job than the existing test suite ?

Also, what platforms would you verify it for ? SQLite is supposed to work with all C compilers, on a wide variety of platforms. Just because it works with one combination, doesn't mean it works for others. How would you finance the collection and maintenance of all the possible platforms SQLite might be used on ?