Proj THUDBFuzz Paper Reading: Query-Aware Test Generation Using a Relational Constraint Solver

Abstract

目的: 使用Alloy tool set对DBMS做黑盒测试
步骤:

1. 输入: a database schema & an SQL query
2. formulate Alloy models for both inputs
   • Q: 这里的both是什么意思？难道不是只有一个input query??
   • Answer: 最后发现是这个工具是用户需要提供数据库Schema（有几张表，主键外键），然后给定查询query（支持SELECT, from, and, or, not, join)，工具会尽量随机给出一个较小的数据库，并且给出查询query的结果，为了提升覆盖率，工具会尽量覆盖数据的等价类，比如select x where x > 3；工具就会生成x > 3和x<=3的，把这两个等价类都照顾到。
3. 使用Alloy来生成一个完全的包含了input和oracle的测试套件。use the Alloy Analyzer to generate:
   1. input data
   2. the expected result
      生成工具: ADUSA
      实验: 显示能够找到bugs

Intro

目前的自动DB testing一般需要

1. SQL queries
2. test databases
3. Oracles
   已有进展
4. RAGS和QGEN能随机将SQL语句结合在一起来生成valid queries
5. 有研究针对又cardinality constraints的queries
6. 一些研究能生成满足指定schema的constraints的数据库，但是这些数据库是query unaware的（不需要提供query信息）
   本文提供了基于黑盒测试的model-based testing方法
   主要方式：
7. 使用Alloy（一种可分析的关系型语言）将输入的db schema和input SQL query转化为对应的Alloy specification(use Alloy to model the inputs)，
8. 使用Alloy Analyzer（本文写的）来生成bounded non-isomorphic databases和预期inputs

本文实现工具：ADUSA
实验：
测试对象：HSQLDB，MySQL，Oracle11g
应用前景：ADUSA+ SQL query generator就能测数据库

Overview

Alloy是一种strongly typed specification langs，有多个paragraphs，用来定义型类型，引入类型间关系或者为类型or关系添加constraints

Alloy示例

对于这样一张表：

CREATE TABLE student ( id int, name varchar(50), PRIMARY KEY (id) );

对应Alloy标准

//定义varchar这个类型，Alloy只支持整数默认类型
sig varchar{} 

one sig student { 
      rows: Int -> varchar 
}{ 
//PRIMARY KEY
      all x: rows.varchar | one x.rows 
}

对于这样一个查询

SELECT DISTINCT id FROM student WHERE (id=1 OR (id>=3 AND id<=5)); 

对应Alloy

fun query () : Int { {select[where[from[student.rows]]]} } 
fun select (rows: Int -> varchar) : Int { {rows.varchar} } 
fun where(rows: Int -> varchar) : Int -> varchar { {x1: rows.varchar, x2: x1.rows | condition[x1]} } 
pred condition(x1: Int) { {eq[x1, 1] or (gte[x1, 3] and lte[x1, 5] )} } 
fun from(rows: Int -> varchar) : Int -> varchar { {rows} }

然而可惜的是我没看到DISTINCT的建模或者是DISTINCT能被支持这一点。虽然id当然是distinct的。
Alloy Analyzer则会试图枚举每个等价类，找到全部instances。不过每种类型的data elements个数是有限制的。可以指定，例如 run query for exactly 2 varchar

生成query

用了off-the-shelf SAT来举出instances

生成Test oracle

Alloy

ADUSA framework

在创建时支持create table语句，primary key以及foreign key两种关系
在查询时支持select语句，支持from,join(cross join, natural join)
对于变量是先建模对应的数据类型为一个空的数据类型，然后再让该变量成为一个单例类

Case Studies

Oracle 11g

1. 为何选这个数据库
2. 实验:
   • 使用的schema和query
   • ADUSA会结束，结束的条件
   • 意义：
     - Fig8成功找到了不连续性
     - 生成速度比较快
     - 用Fig8说明计算的结果是正确的

MySQL

指出了bug编号

HSQLDB

用了注入bug的方法，成功检查到了对应bug
注入的是什么bug，方式（跑一遍原先的，再跑一遍注入了bug的，进行对比）

Discussion

还做不到每种数据生成太多元素，以及还做不到正则表达式等复杂类型