Security Vulnerabilities found in sqlite3.c
(1) By janislley oliveira (janislley) on 2022-01-20 02:03:37 [link] [source]
Hello, 7 potential software vulnerabilities were found in sqlite3.c function. To identify this kind of vulnerabilities I used tool ESBMC-WR: https://github.com/thalestas/esbmc-wr More about the tool: https://arxiv.org/pdf/2102.02368.pdf Please, check the logs of analysis: Issue #1 -------- State 3 file sqlite3.c line 128672 function setAllPagerFlags thread 0 ---------------------------------------------------- pDb = invalid-object State 5 file sqlite3.c line 128673 function setAllPagerFlags thread 0 ---------------------------------------------------- n = 1073741824 (01000000 00000000 00000000 00000000) State 11 file sqlite3.c line 68317 function sqlite3BtreeSetPagerFlags thread 0 ---------------------------------------------------- pBt = invalid-object State 18 file sqlite3.c line 14863 function sqlite3_mutex_try thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 14863 function sqlite3_mutex_try dereference failure: NULL pointer Issue #2 -------- State 6 file sqlite3.c line 32120 function sqlite3AtoF thread 0 ---------------------------------------------------- zEnd = 0 + 1073754047 State 24 file sqlite3.c line 32160 function sqlite3AtoF thread 0 ---------------------------------------------------- z = 0 + 1 State 34 file sqlite3.c line 32177 function sqlite3AtoF thread 0 ---------------------------------------------------- z = 0 + 1 State 54 file sqlite3.c line 32373 function sqlite3Atoi64 thread 0 ---------------------------------------------------- zEnd = invalid-object State 56 file sqlite3.c line 32386 function sqlite3Atoi64 thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 32386 function sqlite3Atoi64 dereference failure: invalid pointer zNum < zEnd => (signed long int)((unsigned char)(*zNum)) >= 0 Issue #3 -------- State 2 file sqlite3.c line 82639 function sqlite3VdbeOneByteSerialTypeLen thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 82639 function sqlite3VdbeOneByteSerialTypeLen array bounds violated: array `sqlite3SmallTypeSizes' upper bound (signed long int)serial_type < 128 Issue #4 -------- State 3 file sqlite3.c line 144325 function sqlite3VtabMakeWritable thread 0 ---------------------------------------------------- pToplevel = ( struct Parse *)(invalid-object) State 6 file sqlite3.c line 144333 function sqlite3VtabMakeWritable thread 0 ---------------------------------------------------- n = 776 (00000000 00000000 00000011 00001000) State 8 file sqlite3.c line 14863 function sqlite3MallocSize thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 14863 function sqlite3MallocSize dereference failure: NULL pointer Issue #5 -------- State 1 file sqlite3.c line 32009 function sqlite3_strnicmp thread 0 ---------------------------------------------------- a = 0 State 2 file sqlite3.c line 32010 function sqlite3_strnicmp thread 0 ---------------------------------------------------- b = invalid-object State 3 file sqlite3.c line 32011 function sqlite3_strnicmp thread 0 ---------------------------------------------------- N = -2147483647 (10000000 00000000 00000000 00000001) State 8 file sqlite3.c line 32012 function sqlite3_strnicmp thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 32012 function sqlite3_strnicmp dereference failure: invalid pointer !(N < 0) => (signed long int)(*b) >= 0 Issue #6 -------- State 2 file sqlite3.c line 53714 function subjRequiresPage thread 0 ---------------------------------------------------- pPager = invalid-object State 4 file sqlite3.c line 53716 function subjRequiresPage thread 0 ---------------------------------------------------- pgno = 8 (00000000 00000000 00000000 00001000) State 7 file sqlite3.c line 53719 function subjRequiresPage thread 0 ---------------------------------------------------- p = invalid-object State 10 file sqlite3.c line 49535 function sqlite3BitvecTestNotNull thread 0 ---------------------------------------------------- i = 7 (00000000 00000000 00000000 00000111) State 17 file sqlite3.c line 49539 function sqlite3BitvecTestNotNull thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 49539 function sqlite3BitvecTestNotNull division by zero p->iDivisor != 0 Issue #7 -------- State 12 file sqlite3.c line 95937 function vdbeSorterMapFile thread 0 ---------------------------------------------------- pFd = 0 State 22 file sqlite3.c line 95907 function vdbePmaReadVarint thread 0 ---------------------------------------------------- Violated property: file sqlite3.c line 95907 function vdbePmaReadVarint division by zero (signed long int)p->nBuffer != 0
(2) By Richard Hipp (drh) on 2022-01-20 02:29:58 in reply to 1 [source]
Thank you for the report.
It appears that ESBMC-WR is a static analyzer. Static analysis tools are notorious for generating lots of false-positives in SQLite. So even without looking, I'm guessing that will be the case here too. This comes up so often, that I'm going to assume that all of these reports are false-positives until I have hard evidence to the contrary. If you don't have a test case which involves feeding some SQL into a (possibly malformed) SQLite database file and then getting a memory error, then you don't have a vulnerability. And I do not see any test cases here, just abstract warnings about "violated properties". So your title is perhaps an exaggeration. Perhaps a more accurate title would be:
Seven places in SQLite that we cannot prove are not security vulnerabilities.
The second problem is that you did not tell us which version of SQLite you run through ESBMC-WR. Without knowing the precise version (the output of the "SELECT sqlite_source_id()" command) the line-number information in your report is useless to us.
If you will kindly let us know precisely what version of SQLite you are running through ESBMC-WR, I'll see what I can do about restructuring the code in order to help it complete its proofs and stop complaining.