Hello,

We found some potential code failures that might cause a security vulnerability. To identify this kind of vulnerabilities I used tool LSVerifier: https://github.com/janislley/LSVerifier

More about the tool: https://ssvlab.github.io/lucasccordeiro/papers/sbseg2023.pdf

Please, check this report for these 5 code property violations:

1 - Division by zero

[FILE] src/vdbesort.c

[ARGS] ['--unwind', '1', '--no-unwinding-assertions']

[FUNCTION] vdbePmaWriterInit

static void vdbePmaWriterInit(
  sqlite3_file *pFd,              /* File handle to write to */
  PmaWriter *p,                   /* Object to populate */
  int nBuf,                       /* Buffer size */
  i64 iStart                      /* Offset of pFd to begin writing at */
){
  memset(p, 0, sizeof(PmaWriter));
  p->aBuffer = (u8*)sqlite3Malloc(nBuf);
  if( !p->aBuffer ){
    p->eFWErr = SQLITE_NOMEM_BKPT;
  }else{
    p->iBufEnd = p->iBufStart = (iStart % nBuf); // line 1464
    p->iWriteOff = iStart - p->iBufStart;
    p->nBuffer = nBuf;
    p->pFd = pFd;
  }
}

Counterexample:

State 3 file vdbesort.c line 1464 function vdbePmaWriterInit thread 0

Violated property:
file vdbesort.c line 1464 function vdbePmaWriterInit
division by zero
(signed long int)nBuf != 0

line 1464: p->iBufEnd = p->iBufStart = (iStart % nBuf);

The error you've pointed out suggests that there's a potential "Division by Zero" vulnerability in the vdbePmaWriterInit function. Specifically, the vulnerability occurs when the modulo operation iStart % nBuf is executed, and nBuf is zero.

Potential fix:

• Add a check at the beginning of the function to see if nBuf is zero.
• If nBuf is zero, handle the situation appropriately (e.g., set an error code or return early from the function).

2 - Array bounds violated

[FILE] src/func.c [ARGS] ['--unwind', '1', '--no-unwinding-assertions'] [FUNCTION] lowerFunc

static void lowerFunc(sqlite3_context *context, int argc, sqlite3_value **argv){
  char *z1;
  const char *z2;
  int i, n;
  UNUSED_PARAMETER(argc);
  z2 = (char*)sqlite3_value_text(argv[0]);
  n = sqlite3_value_bytes(argv[0]);
  /* Verify that the call to _bytes() does not invalidate the _text() pointer */
  assert( z2==(char*)sqlite3_value_text(argv[0]) );
  if( z2 ){
    z1 = contextMalloc(context, ((i64)n)+1);
    if( z1 ){
      for(i=0; i<n; i++){
        z1[i] = sqlite3Tolower(z2[i]);
      }
      sqlite3_result_text(context, z1, n, sqlite3_free);
    }
  }
}

Counterexample:

State 12 file func.c line 536 function lowerFunc thread 0

Violated property:
file func.c line 536 function lowerFunc
array bounds violated: array `sqlite3UpperToLower' upper bound
(signed long int)((unsigned char)(*(z2 + (signed long int)i))) < 1

line 536: z1[i] = sqlite3Tolower(z2[I]);

VERIFICATION FAILED

The violation occurs when accessing the sqlite3UpperToLower array using the index derived from the z2 string.

• To fix this issue, we need to ensure that the index used to access the sqlite3UpperToLower array is within the valid bounds of the array.

3 - Same object violation

[FILE] src/alter.c [ARGS] ['--unwind', '1', '--no-unwinding-assertions'] [FUNCTION] renameColumnTokenNext

static RenameToken *renameColumnTokenNext(RenameCtx *pCtx){
  RenameToken *pBest = pCtx->pList;
  RenameToken *pToken;
  RenameToken **pp;

  for(pToken=pBest->pNext; pToken; pToken=pToken->pNext){
    if( pToken->t.z>pBest->t.z ) pBest = pToken; // line 1041
  }
  for(pp=&pCtx->pList; *pp!=pBest; pp=&(*pp)->pNext);
  *pp = pBest->pNext;

  return pBest;
}

Counterexample:

State 7 file alter.c line 1041 function renameColumnTokenNext thread 0

Violated property:
file alter.c line 1041 function renameColumnTokenNext
Same object violation
SAME-OBJECT(pToken->t.z, pBest->t.z)

line 1041: if( pToken->t.z>pBest->t.z ) pBest = pToken;

Same Object Violation in the renameColumnTokenNext function. Specifically, the violation occurs when comparing the pointers pToken->t.z and pBest->t.z.

To fix this issue, we need to ensure that we're not comparing pointers that refer to the same object using relational operators.

Potential fix:

• Before the comparison, check if the pointers pToken->t.z and pBest->t.z refer to the same object.
• If they do, handle the situation appropriately (e.g., skip the comparison or use another method to compare the objects).

4 - Division by zero

[FILE] src/hash.c [ARGS] ['--unwind', '1', '--no-unwinding-assertions'] [FUNCTION] rehash

static int rehash(Hash *pH, unsigned int new_size){
  struct _ht *new_ht;            /* The new hash table */
  HashElem *elem, *next_elem;    /* For looping over existing elements */

#if SQLITE_MALLOC_SOFT_LIMIT>0
  if( new_size*sizeof(struct _ht)>SQLITE_MALLOC_SOFT_LIMIT ){
    new_size = SQLITE_MALLOC_SOFT_LIMIT/sizeof(struct _ht);
  }
  if( new_size==pH->htsize ) return 0;
#endif

  sqlite3BeginBenignMalloc();
  new_ht = (struct _ht *)sqlite3Malloc( new_size*sizeof(struct _ht) );
  sqlite3EndBenignMalloc();

  if( new_ht==0 ) return 0;
  sqlite3_free(pH->ht);
  pH->ht = new_ht;
  pH->htsize = new_size = sqlite3MallocSize(new_ht)/sizeof(struct _ht);
  memset(new_ht, 0, new_size*sizeof(struct _ht));
  for(elem=pH->first, pH->first=0; elem; elem = next_elem){
    unsigned int h = strHash(elem->pKey) % new_size; //line 135
    next_elem = elem->next;
    insertElement(pH, &new_ht[h], elem);
  }
  return 1;
}

Counterexample:

State 13 file hash.c line 135 function rehash thread 0

Violated property:
file hash.c line 135 function rehash
division by zero
new_size != 0

line 135: unsigned int h = strHash(elem->pKey) % new_size;

Potential "Division by Zero" vulnerability in the rehash function. Specifically, the vulnerability occurs when the modulo operation strHash(elem->pKey) % new_size is executed, and new_size is zero.

To fix this issue, you should ensure that new_size is never zero before performing the modulo operation.

Potential fix:

• Add a check after the assignment of new_size to see if new_size is zero.
• If new_size is zero, handle the situation appropriately (e.g., set an error code, free any allocated memory, or return early from the function).

5 - Dereference failure: NULL pointer

[FILE] src/memdb.c [ARGS] ['--unwind', '1', '--no-unwinding-assertions'] [FUNCTION] memdbFromDbSchema

static MemFile *memdbFromDbSchema(sqlite3 *db, const char *zSchema){
  MemFile *p = 0;
  MemStore *pStore;
  int rc = sqlite3_file_control(db, zSchema, SQLITE_FCNTL_FILE_POINTER, &p);
  if( rc ) return 0;
  if( p->base.pMethods!=&memdb_io_methods ) return 0; // line 739
  pStore = p->pStore;
  memdbEnter(pStore);
  if( pStore->zFName!=0 ) p = 0;
  memdbLeave(pStore);
  return p;
}

Counterexample:

State 1 file memdb.c line 737 function memdbFromDbSchema thread 0

State 2 file memdb.c line 739 function memdbFromDbSchema thread 0

Violated property:
file memdb.c line 739 function memdbFromDbSchema
dereference failure: NULL pointer

line 739: if( p->base.pMethods!=&memdb_io_methods ) return 0;

A potential null pointer dereference. The code assumes that after the sqlite3_file_control call, the pointer p is valid. However, there's no explicit check to ensure that p is not null before it's dereferenced in the line:

To fix this potential vulnerability, you should add a null check for p after the sqlite3_file_control call and before any dereference of p.