生成数据库
以下为各种语言创建数据库的命令。
1 | java |
CodeQL
不支持PHP
,支持的编程语言类型,参考官网[1]。对于Java
代码有些不同,需要进行代码的编译后[2],才能生成相关的数据库。
编译过程中,若出现环境问题可使用--verbose
输出详细的错误,进行错误的定位。
1 | codeql database create webgoat-qldb -language= java --command "./mvnw clean package -DskipTests" --verbose |
对于Java
代码的特殊性[3],,实战中获取到的可能是编译后的Java
代码,这里可以使用工具CodeQLpy
[4],它可以对多种不同类型的java代码进行代码审计,包括jsp文件、SpringMVC的war包、SpringBoot的jar包、maven源代码。
基础语法结构
Codeql
查询语法有点类似SQL
查询,结构如下:
1 | /** |
编写第一个查询
创建第一个QL包
这里以WebGoat
[5]创建的数据库为查询对象。
创建一个文件夹,用来存放后续你编写的CodeQL
脚本,CodeQL
官方称这个文件夹为QL Pack
。
例如名为qltest
的文件夹,并在里面创建1个QL Pack
的配置文件,名称固定为qlpack.yml
。再创建一个ql后缀的文件,名称随意。
qlpack.yml
文件中写入以下内容:
1 | name: qltest |
-
第一行表示这个QL包的名称为
qltest
,必选,如果你在VSCode中同时打开多个QL包时,要保证这个name的值唯一不重复。 -
第二行表示这个QL包的版本号,必选。
-
第三行表示这个QL包的依赖,必选,codeql-java表示需要Java语言的QL标准库依赖。
在VSCode的CodeQL插件中添加用CodeQL创建的WebGoat的数据库
编写查询
在webgoat-query.ql
文件中编写如下代码,用来查找WebGoat项目中所有声明的方法。
1 | import java |
然后右键点击webgoat-query.ql
文件,点击【CodeQL: Run Query 】来执行本次查询,执行完成后在右边可以看到多出一列用来显示查询结果。
QL语言参考
- 关于 QL 语言:QL 是 CodeQL 的强大查询语言,用于分析代码。
- 谓词:谓词用于描述构成 QL 程序的逻辑关系。
- 查询:查询是 QL 程序的输出。他们评估结果集。
- 类型:QL 是一种静态类型语言,因此每个变量都必须有一个声明的类型。
- 模块:模块提供了一种通过将相关类型、谓词和其他模块组合在一起来组织 QL 代码的方法。
- 别名:别名是现有 QL 实体的替代名称。
- 变量:QL 中的变量与代数或逻辑中的变量的使用方式类似。它们代表一组值,这些值通常受公式限制。
- 表达式:表达式计算为一组值并具有类型。
- 公式:公式定义了表达式中使用的自由变量之间的逻辑关系。
- 注释:注释是一个字符串,您可以将其直接放在 QL 实体或名称的声明之前。
- 递归:QL 为递归提供了强大的支持。如果 QL 中的谓词直接或间接依赖于自身,则称其为递归谓词。
- 词法语法:QL 语法包括不同种类的关键字、标识符和注释。
- 名称解析:QL 编译器将名称解析为程序元素。
- QL方案的评价:以多个不同的步骤评估QL程序。
- QL 语言规范:QL语言的形式规范。它为术语,语法和有关QL的其他技术细节提供了全面的参考。
谓词Predicates
官方文档[6] ,谓词(Predicates)有点类似于其他语言中的函数,但又与函数不同,谓词用于描述构成 QL 程序的逻辑关系。确切的说,谓词描述的是给定参数与元组集合的关系。
定义谓词有以下几个注意点(坑点):
- 需要注意的是谓词的名字开头必须是小写字母。
- 绑定行为与绑定集。
无结果谓词
没有结果的谓词以predicate作为开头,剩下的语法结构类似于定义函数。这种谓词只能在where语句中使用[7]。
例子如下:
1 | predicate isCity(string city) { |
结果谓词
有结果的谓词的定义类似于C/C++
语言的函数定义,已返回类型替代predicate
作为开头。这种谓词可以在where
与select
语句中使用。
简单的例子如下:
1 | int addOne(int i) { |
递归谓词
这里说的递归并非我们常规理解的函数递归,我们可以理解为一个可反向查找的谓词,或者换一个思维,把非递归的结果谓词理解为一个有向图,那么递归的结果谓词可以理解为一个无向图。
1 | string getANeighbor(string country) { |
输出结果如下:
输出的结果为:France
、Austria
、Belgium
。
为什么会有France
呢?
因为getANeighbor("Germany")
,由
1 | country = "Germany" and result = "Austria" |
可以得到Austria、Belgium
。
这里的递归不是单向的,而是双向的,由于存在France -> Germany
,所以由Germany
可以反向递归得到France
这个结果。
特征谓词、非成员谓词、成员谓词
谓词分为三种,即非成员谓词、成员谓词语和特征谓词。
-
非成员谓词是在类之外定义的,它们不是任何类的成员。
-
成员谓词则是在类里面定义的。
-
特征谓词则是类中的特殊谓词。
类似于其他语言中类的构造函数。
每种谓词的示例:
1 | int getSuccessor(int i) { // 1. 非成员谓词(Non-member predicate) |
绑定行为与绑定集
谓词只能包含有限数量的元组。
正例:
1 | // 正例,i被限定在1到10内,或者你也可以给i赋一个确定的值如i=1 |
反例:
1 | // 反例,i是无限数量值的,此时CodeQL编译器会报错: The body of this 'test::addOne' does not bind 'result' to a value. |
单个绑定集
为了使上述的反例谓词能够通过编译,我们可以使用绑定集(bindingset),但是当我们去调用这个谓词时,传递的参数还是只能在有限的参数集中。
上面的反例可以修改为如下:
1 | bindingset[i] |
多个绑定集
我们同样可以添加多个绑定集,下面是一个例子:
1 | bindingset[x] bindingset[y] |
这个绑定集的意思是如果x或y绑定(bound)了,那么x和y都绑定,即至少有一个参数受到约束。
如果我们想要两者都受约束,可以将例子修改一下:
1 | bindingset[x, y] |
那么这个谓词就变为了一个类似于校验的函数,即x+1 == y
。
查询Queries
官方文档[8],查询是CodeQL
的输出。查询的两种类型,分别是
select
子句- 查询谓语,意味着我们可以从当前模块中定义或者从其他模块中导入。
select子句
子句的格式如下:
1 | from /* ... variable declarations ... */ |
from
和where
部分是可选的。我们可以在from
中定义变量,在where
中给变量赋值和对查询结果的过滤,最后在select
中显示结果。
在select
后面除了表达式(expressions
)之外,还可以使用一些关键字:
as
关键字,后面跟随一个名字。作用相当于sql中的as
,为结果列提供了一个"标签",并允许在后续的select
表达式中使用它们。order by
关键字,后面跟随一个结果列名。作用相当于sql中的order by
,用于排序结果,并且在结果列名后可选asc
(升序)或desc
(降序)关键字。
as
关键字,例子如下:
1 | from int x, int y |
order by
关键字,如下:
1 | from int x, int y |
查询谓词
查询谓词是一个非成员谓词,并在最开头使用query
作为注解。它返回谓词计算结果的所有元组,下面是一个简单的示例:
例如:
1 | query int getProduct(int x, int y) { |
编写查询谓词而不是select
子句的一个好处是,你也可以在代码的其它部分调用谓词。select
子句就像一个匿名谓词,你以后无法调用它。
例如, 我们可以在类中的特征谓词内部调用:
1 | query int getProduct(int x, int y) { |
这样我们查询结果就有2个,一个是内置的#select
,一个是getProduct
,#select
的结果如下:
类型Types
QL
是一种静态类型语言,因此每个变量都必须具有声明类型。
类型是一组值。例如,类型int
是整数的集合。注意⚠️,一个值可以属于多个集合,这意味着它可以有多种类型。
QL
中的类型有原始类型(primitive types
)、类(classes
)、字符类型(character types
)、类域类型(class domain types
)、代数数据类型(algebraic datatypes
)、类型联合(type unions
)和数据库类型(database types
)。
原始类型(Primitive types)
这些类型内置于 QL 中,并且始终在全局命名空间中可用,独立于您正在查询的数据库。
- boolean : 此类型包含值
true
和false
。 - float : 此类型包含64位浮点数,例如
6.28
和-0.618
- int : 此类型包含 32 位二进制补码整数,例如
-1
和42
。 - string : 此类型包含 16 位字符的有限字符串。
- data : 此类型包含日期(也可以包含时间)。
QL 在基本类型上定义了一系列内置操作。这些操作可以通过使用 .
的方式进行调用。例如, 1.toString()
是整数常量1
的字符串表示。有关 QL 中可用的内置操作的完整列表,请参阅 QL 语言规范中的内置操作部分。
此外, QlBuiltins::BigInt有一个任意范围的整数原始类型
类(Classes)
你可以在QL
中定义自己的类型。一种方法是定义一个类。
类提供了一种简单的方法来重写和构造代码。例如,你可以:
- 将相关值组合在一起。
- 根据这些值定义成员谓词。
- 定义子类以重写成员谓词。
QL 中的类不会“创建”新对象,它仅表示逻辑属性。如果某个值满足该逻辑属性,则该值属于特定类。
定义一个类型(Defining a class)
要定义一个类,你可以这样写:
- 关键字
class
- 类的名称。这是一个标识符 以大写字母开头。
- 改类通过
extends
和/
或instanceof
关联父类型(supertypes
)。 - 类的主体,用括号括起来。
定义类的格式,例如:
1 | class ClassName [extends Parent] { |
类名首字母必须是大写⚠️,例如:
1 | class OneTwoThree extends int { |
这定义了一个类OneTwoThree
,它包含值1
,2
和3
。 特征谓词捕捉 “是整数 1、2 或 3 之一” 的逻辑属性。
OneTwoThree
扩展了int
,也就是说,它是int
的子类型。QL
中的类必须始终具有至少一个父类型(supertypes
)。使用extends
关键字引用的父类型称为类的基类型(base types
)。类的值包含在父类型的交集中(即,它们位于类的域类型中)。类从其基类型继承所有成员谓词。
一个类可以扩展多种类型。更多信息,请参阅" 多重继承 "。一个类可以扩展final
类型(或final
类型的别名),请参阅"final 扩展 “。类还可以特化其他类型,而无需通过instanceof
扩展类接口,请参阅” 不扩展子类型 "。
在CodeQL
中,类允许多重继承,但是以下操作是非法的:
- 不能继承本身
- 不能继承
final
类 - 不能继承不兼容的类型,请参考" 类型兼容性 "。
你也可以为类添加注解。可以查看类的注解列表。
类主体(Class bodies)
类的主体可以包含:
当你定义一个类时,该类还会从其父类型继承所有非私有成员谓词和字段。
根据它们是否是final
的,你可以重写(override
)或 隐藏(shadow
)这些谓词和字段以赋予它们更具体的定义。
特征谓词(Characteristic predicate)
类似于其他语言中类的构造函数,只能定义一个,我们可以在特征谓词中使用this
来限制类中可能的值。在上述例子中,OneTwoThree
被限制为1-3
中的整数。
成员谓词(Member predicate)
这些谓词仅适用于类中。我们可以这样去调用类的成员谓词:
1 | class OneTwoThree extends int { |
结果为:
表达式(OneTwoThree
)是一个强制类型转换 。它确保1
具有类型OneTwoThree
而不仅仅是int
。因此,它可以访问成员谓词getAString()
。
还可以这样调用,例如,你可以使用string
定义的内置函数toUpperCase()
:
1 | select 1.(OneTwoThree).getAString().toUpperCase() |
字段(Field)
这些是在类主体中声明的变量。类主体中可以有任意数量的字段声明。你可以在类内部的谓词声明中使用这些变量。与变量 this
类似,字段必须在特征谓词 中受到约束。
一个简单的例子如下,它输出10
以内每个数字的除数:
1 | class SmallInt extends int { |
输出的结果如下:
具体类(Concrete classes)
上述所提到的类都是具体的类,具体类是通过限制较大类型中的值来定义的。
抽象类(Abstract classes)
带有 abstract
注释的类称为抽象类。具体而言,对于抽象类中的值,它必须满足类本身的特征谓词和子类的特征谓词。请注意,在这种情况下, final 扩展不被视为子类。
如果您想将多个现有类归类到一个通用名称下,抽象类就非常有用。然后,您可以在所有这些类上定义成员谓词。你还可以扩展预定义的抽象类:例如,如果你导入一个包含抽象类的库,则可以为其添加更多子类。
例子:
希望识别所有可解释为 SQL 查询的表达式。您可以使用以下抽象类来描述这些表达式:
1 | abstract class SqlExpr extends Expr { |
现在定义各种子类——每种数据库管理系统对应一个。例如,您可以定义一个子类 class PostgresSqlExpr extends SqlExpr
,它包含传递给执行数据库查询的Postgres API
的表达式。你也可以为MySQL
和其他数据库管理系统定义类似的子类。
重写成员谓词(Overriding member predicates)
如果一个类从非final
的父类型继承了成员谓词,则可以重写继承的定义。为此,你可以定义一个与继承谓词具有相同名称和属性的成员谓词,并添加 override
注解 。
例如,扩展了一下前面的例子:
OneTwo
的getAstring()
覆盖了原来的OneTwoThree
的getAstring()
。
1 | class OneTwoThree extends int { |
输出的结果如下:
再加一个TwoThree
,继续重写getAString()
。
1 | class OneTwoThree extends int { |
运行输出的结果为:
多重继承(Multiple inheritance)
一个类可以扩展多种类型。在这种情况下,它会继承自所有这些类型。
例如:
1 | class Two extends OneTwo, TwoThree {} |
这个类Two
同时继承了OneTwo
和TwoThree
,它还间接继承自OneTwoThree
和int
,那么通过特征谓词我们知道其值只能是2。
如果一个子类继承了同一个谓词的多个定义,那么该类还需要手动重写该谓词以避免歧义,在这种情况下我们可以考虑使用super
表达式。
例如:
1 | class Two extends OneTwo, TwoThree { |
Final拓展(Final extensions)
类可以扩展final
类型或final
类型的别名。在这种情况下,它会继承这些父类型的所有成员谓词和字段的final
版本。通过final
扩展继承的成员谓词无法被覆盖,但可以被隐藏。
例如:
1 | class OneTwoThree extends int { |
运行的结果如下:
修改为:from OneTwoFinalExtension o select o, o.getAString()
当在OneTwoFinalExtension
上调用getAString()
时,原始定义被屏蔽了。结果如下:
变量Variables
QL 中的变量使用方式与代数或逻辑中的变量类似。它们表示一组值,这些值通常受公式(formula
)约束。
这与其他一些编程语言中的变量不同,在其他编程语言中,变量代表可能包含数据的内存位置。这些数据也可能随时间而变化。例如,在 QL
中, n = n + 1
是一个等式公式 ,仅当 n
等于 n + 1
时才成立(因此实际上它对任何数值都不成立)。在Java
中, n = n + 1
不是等式,而是一个赋值操作,它通过在当前值上加 1
来更改 n
的值。
声明变量(Declaring a variable)
所有变量声明都由变量类型和名称组成。名称可以是任何标识符 以小写字母开头。
例如, int i
、 SsaDefinitionNode node
和 LocalScopeVariable lsv
声明变量 i
、 node
和 lsv
的类型为 int
、 SsaDefinitionNode
和 LocalScopeVariable
变量声明出现在不同的上下文中,例如在选择子句中、在量化公式中、作为谓词的参数等等。
从概念上讲,你可以认为变量保存了其类型允许的所有值,但要受到任何进一步的约束⚠️。
例如,考虑以下选择子句:
1 | from int i |
仅根据变量 i
的类型,它可以包含所有整数。然而,它受到公式 i in [0 .. 9]
的限制。因此,select
子句的结果是从0
到9
之间的10
个数字(含 0
和 9
)。
另外,请注意⚠️查询会导致编译时错误:
1 | from int i |
理论上,它会有无限多个结果,因为变量i
的可能值并不受限于有限个。想了解更多,可参阅“ 绑定 ”。
自由变量和绑定变量(Free and bound variables)
变量可以扮演不同的角色。有些变量是自由变量 ,它们的值直接影响使用它们的表达式的值,或者 使用它们的公式是否成立。其他变量被称为绑定变量,它们被限制在特定的值集内。
例子如下:
1 | "hello".indexOf("l") |
第一个表达式没有任何变量。它查找字符串 "hello"
中 "l"
出现的(从零开始的)索引,因此其计算结果为 2
和 3
。
第二个表达式的计算结果为 -3
,即 [-3 .. 3]
范围内的最小值。虽然此表达式使用了变量 f
,但它只是一个占位符或“虚拟”变量,您无法为其赋值。您可以将 f
替换为其他变量,而不会改变表达式的含义。例如, min(float f | f in [-3 .. 3])
始终等于 min(float other | other in [-3 .. 3])
. 这是绑定变量的一个例子。
对于表达式 (i + 7) * 3
和 x.sqrt()
。在这两个例子中,表达式的值取决于变量 i
和 x
分别被赋值的值。换句话说,变量的值会影响表达式的值。这些都是自由变量的例子。
类似地,如果公式包含自由变量,则该公式是否成立取决于分配给这些变量的值。例如:
1 | "hello".indexOf("l") = 1 |
-
第一个公式不包含任何变量,并且永远不会成立(因为
"hello".indexOf("l")
具有值2
和3
,而没有1
)。 -
第二个公式仅包含一个绑定变量,因此不受该变量变化的影响。由于
min(float f | f in [-3 .. 3])
等于-3
,因此该公式始终成立。 -
第三个公式包含一个自由变量
i
。公式是否成立取决于赋给i
值。例如,如果赋给i
值为1
或2
(或任何其他int
),则公式成立。另一方面,如果赋给i
值为3.5
,则公式不成立。
第四个公式包含一个自由变量 x
和一个绑定变量 y
。如果 x
被赋值为非负数,则最后一个公式成立。另一方面,如果 x
被赋值为 例如 -9
,则公式不成立。变量 y
不会影响公式是否成立。
表达式Expressions
表达式计算一组值并具有类型。例如,表达式 1 + 2
计算结果为整数 3
,表达式 "QL"
计算结果为字符串 "QL"
。1 1 + 2
类型为 int
,而 "QL"
类型为 string
。本小节只讲述父类表达式,其它可参考[9]。
父类表达式(Super expressions)
QL
中的父类表达式与其他编程语言(例如Java
)中的父类表达式类似。当您想要使用父类型的谓词定义时,可以在谓词调用中使用它们。实际上,当谓词从其父类型继承两个定义时,这很有用。在这种情况下,谓词必须重写 这些定义是为了避免歧义。 但是,如果你想使用特定超类型的定义,而不是编写新的定义,可以使用父类表达式。
在下面的例子中,类 C
继承了谓词的两个定义 getANumber()
— 一个来自 A
,一个来自 B
。它不会重写两个定义,而是使用 B
中的定义。
1 | class A extends int { |
该查询的结果为:
公式Formulas
公式定义表达式中使用的自由变量之间的逻辑关系。
根据赋予这些自由变量的值,公式可能为真或为假。当公式为真时,我们通常说该公式成立 。
例如,如果将值 9
赋给 x
,公式 x = 4 + 5
成立,但对于其他赋值,公式 x
= 4 + 5 不成立。有些公式没有任何自由变量。例如, 1 < 2
始终成立,而 1 > 2
永远不会成立。
下面只介绍个人认为比较特殊的点,其它点较为简单,可参考原文[10]。
顺序(Order)
要使用这些顺序运算符之一比较两个表达式,每个表达式必须具有一个类型,并且这些类型必须兼容并且 可排序的 。
这些符号为:>、>=、<、<=
例如,公式 "Ann" < "Anne"
和 5 + 6 >= 11
均成立。
注解Annotations
注释是一个字符串,您可以将其直接放置在QL
实体或名称的声明之前。类似于Java
语言。
例如,要将模块 M
声明为私有的,您可以使用:
1 | private module M { |
请注意,一些注释作用于实体本身,而其他注释作用于实体的特定名称 :
-
对实体进行操作:
abstract
、cached
、external
、transient
、override
、pragma
、language
和bindingset
-
对名称进行操作:
deprecated
、library
、private
、final
和query
例如,如果你使用 private
注释一个实体,那么只有该特定名称是私有的。你仍然可以使用其他名称(使用 alias )访问该实体。另一方面,如果您使用 cached
注释一个实体,那么该实体本身将被缓存。
具体的例子:
1 | module M { |
在这种情况下,查询 select M::foo()
会报错,因为名称 foo
是私有的。查询 select M::bar()
是有效的(返回结果 1
),因为名称 bar
是可见的,并且它是谓词 foo
的别名。
参考
https://codeql.github.com/docs/codeql-overview/supported-languages-and-frameworks/ ↩ ↩︎
https://codeql.github.com/docs/ql-language-reference/predicates/ ↩︎
https://codeql.github.com/docs/ql-language-reference/queries/# ↩︎
https://codeql.github.com/docs/ql-language-reference/expressions/# ↩︎
https://codeql.github.com/docs/ql-language-reference/formulas/#formulas ↩︎