Codeql查询语法笔记

生成数据库

以下为各种语言创建数据库的命令。

# java
codeql database create "~/CodeQL/databases/code-database" --source-root="~/CodeQL/projects/java-code" --language=java --command="mvn clean install -file pom.xml"
# Go
codeql database create "~/CodeQL/databases/code-database" --source-root="~/CodeQL/projects/java-code" --language=go
# Python
codeql database create "~/CodeQL/databases/code-database" --source-root="~/CodeQL/databases/code-database" --language=python
# JavaScript
codeql database create "~/CodeQL/databases/code-database" --source-root="~/CodeQL/databases/code-database" --language=javascript

CodeQL不支持PHP，支持的编程语言类型，参考官网^[1]。对于Java代码有些不同，需要进行代码的编译后^[2]，才能生成相关的数据库。

编译过程中，若出现环境问题可使用--verbose输出详细的错误，进行错误的定位。

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查询，结构如下：

/**
 *
 * Query metadata
 *
 */

import /* ... CodeQL libraries or modules ... */

/* ... Optional, define CodeQL classes and predicates ... */

from /* ... 变量声明 ... */
where /* ... 逻辑处理 ... */
select /* ... 表达式 ... */

编写第一个查询

创建第一个QL包

这里以WebGoat^[5]创建的数据库为查询对象。

创建一个文件夹，用来存放后续你编写的CodeQL脚本，CodeQL官方称这个文件夹为QL Pack。

例如名为qltest的文件夹，并在里面创建1个QL Pack的配置文件，名称固定为qlpack.yml。再创建一个ql后缀的文件，名称随意。

qlpack.yml文件中写入以下内容：

name: qltest
version: 0.0.0
libraryPathDependencies: codeql-java

• 第一行表示这个QL包的名称为qltest，必选，如果你在VSCode中同时打开多个QL包时，要保证这个name的值唯一不重复。

• 第二行表示这个QL包的版本号，必选。

• 第三行表示这个QL包的依赖，必选，codeql-java表示需要Java语言的QL标准库依赖。

在VSCode的CodeQL插件中添加用CodeQL创建的WebGoat的数据库

编写查询

在webgoat-query.ql文件中编写如下代码，用来查找WebGoat项目中所有声明的方法。

import java

from Method m
select m

然后右键点击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 程序的逻辑关系。确切的说，谓词描述的是给定参数与元组集合的关系。
定义谓词有以下几个注意点(坑点)：

1. 需要注意的是谓词的名字开头必须是小写字母。
2. 绑定行为与绑定集。

无结果谓词

没有结果的谓词以predicate作为开头，剩下的语法结构类似于定义函数。这种谓词只能在where语句中使用^[7]。

例子如下：

predicate isCity(string city) {
city = "Beijing"
or
city = "ShangHai"
}

from string city
where city = "Beijing" and isCity(city)
select city

结果谓词

有结果的谓词的定义类似于C/C++语言的函数定义，已返回类型替代predicate作为开头。这种谓词可以在where与select语句中使用。

简单的例子如下：

int addOne(int i) {
    result = i + 1 and
    i in [1 .. 10]
}

from int v
where v = 1
select addOne(v)

递归谓词

这里说的递归并非我们常规理解的函数递归，我们可以理解为一个可反向查找的谓词，或者换一个思维，把非递归的结果谓词理解为一个有向图，那么递归的结果谓词可以理解为一个无向图。

string getANeighbor(string country) {
    country = "France" and result = "Belgium"
    or
    country = "France" and result = "Germany"
    or
    country = "Germany" and result = "Austria"
    or
    country = "Germany" and result = "Belgium"
    or
    country = getANeighbor(result)
  }

from string people
where people = getANeighbor("Germany")
select people

输出结果如下：

输出的结果为：France、Austria、Belgium。

为什么会有France呢？

因为getANeighbor("Germany")，由

country = "Germany" and result = "Austria"
or
country = "Germany" and result = "Belgium"

可以得到Austria、Belgium。

这里的递归不是单向的，而是双向的，由于存在France -> Germany，所以由Germany可以反向递归得到France这个结果。

特征谓词、非成员谓词、成员谓词

谓词分为三种，即非成员谓词、成员谓词语和特征谓词。

• 非成员谓词是在类之外定义的，它们不是任何类的成员。

• 成员谓词则是在类里面定义的。

• 特征谓词则是类中的特殊谓词。

类似于其他语言中类的构造函数。

每种谓词的示例：

int getSuccessor(int i) {  // 1. 非成员谓词(Non-member predicate)
  result = i + 1 and
  i in [1 .. 9]
}

class FavoriteNumbers extends int {
  FavoriteNumbers() {  // 2. 特征谓词(Characteristic predicate)
    this = 1 or
    this = 4 or
    this = 9
  }

  string getName() {   // 3. 成员谓词(Member predicate) for the class `FavoriteNumbers`
    this = 1 and result = "one"
    or
    this = 4 and result = "four"
    or
    this = 9 and result = "nine"
  }
}

绑定行为与绑定集

谓词只能包含有限数量的元组。

正例：

// 正例，i被限定在1到10内，或者你也可以给i赋一个确定的值如i=1
int addOne(int i) {
    result = i + 1 and
    i in [1 .. 10]
}

反例：

// 反例，i是无限数量值的，此时CodeQL编译器会报错: The body of this 'test::addOne' does not bind 'result' to a value.
int addOne(int i) {
    result = i + 1 and
    i > 0
}

单个绑定集

为了使上述的反例谓词能够通过编译，我们可以使用绑定集(bindingset)，但是当我们去调用这个谓词时，传递的参数还是只能在有限的参数集中。
上面的反例可以修改为如下：

bindingset[i]
int addOne(int i) {
    result = i + 1 and
    i > 0
}

// 此时我们可以去调用这个谓词，但是需要注意传递过来的参数还是只能在有限的参数集中
from int i
where i = 1
select addOne(i)

多个绑定集

我们同样可以添加多个绑定集，下面是一个例子:

bindingset[x] bindingset[y]
predicate plusOne(int x, int y) {
  x + 1 = y
}
    
from int z
where z= 2 and plusOne(1, z)
select z

这个绑定集的意思是如果x或y绑定(bound)了，那么x和y都绑定，即至少有一个参数受到约束。
如果我们想要两者都受约束，可以将例子修改一下:

bindingset[x, y]
predicate plusOne(int x, int y) {
  x + 1 = y
}

那么这个谓词就变为了一个类似于校验的函数，即x+1 == y。

查询Queries

官方文档^[8]，查询是CodeQL的输出。查询的两种类型，分别是

• select子句
• 查询谓语，意味着我们可以从当前模块中定义或者从其他模块中导入。

select子句

子句的格式如下：

from /* ... variable declarations ... */
where /* ... logical formula ... */
select /* ... expressions ... */

from和where部分是可选的。我们可以在from中定义变量，在where中给变量赋值和对查询结果的过滤，最后在select中显示结果。

在select后面除了表达式(expressions)之外，还可以使用一些关键字：

• as关键字，后面跟随一个名字。作用相当于sql中的as，为结果列提供了一个"标签"，并允许在后续的select表达式中使用它们。
• order by关键字，后面跟随一个结果列名。作用相当于sql中的order by，用于排序结果，并且在结果列名后可选asc(升序)或desc(降序)关键字。

as关键字，例子如下：

from int x, int y
where x = 3 and y in [0 .. 2]
select x, y, x * y as product, "product: " + product

order by关键字，如下：

from int x, int y
where x = 3 and y in [0 .. 2]
select x, y, x * y as product, "product: " + product order by y desc

查询谓词

查询谓词是一个非成员谓词，并在最开头使用query作为注解。它返回谓词计算结果的所有元组，下面是一个简单的示例:

例如：

query int getProduct(int x, int y) {
  x = 3 and
  y in [0 .. 2] and
  result = x * y
}

编写查询谓词而不是select子句的一个好处是，你也可以在代码的其它部分调用谓词。select子句就像一个匿名谓词，你以后无法调用它。

例如， 我们可以在类中的特征谓词内部调用：

query int getProduct(int x, int y) {
    x = 3 and
    y in [0 .. 2] and
    result = x * y
}
class MultipleOfThree extends int {
    MultipleOfThree() { 
        this = getProduct(_, _) 
    }
}
from MultipleOfThree m select m

这样我们查询结果就有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 中，并且始终在全局命名空间中可用，独立于您正在查询的数据库。

1. boolean : 此类型包含值true和false。
2. float : 此类型包含64位浮点数，例如6.28和-0.618
3. int : 此类型包含 32 位二进制补码整数，例如-1和42 。
4. string : 此类型包含 16 位字符的有限字符串。
5. data : 此类型包含日期（也可以包含时间）。

QL 在基本类型上定义了一系列内置操作。这些操作可以通过使用 .的方式进行调用。例如， 1.toString()是整数常量1的字符串表示。有关 QL 中可用的内置操作的完整列表，请参阅 QL 语言规范中的内置操作部分。

此外， QlBuiltins::BigInt有一个任意范围的整数原始类型

类(Classes)

你可以在QL中定义自己的类型。一种方法是定义一个类。

类提供了一种简单的方法来重写和构造代码。例如，你可以：

• 将相关值组合在一起。
• 根据这些值定义成员谓词。
• 定义子类以重写成员谓词。

QL 中的类不会“创建”新对象，它仅表示逻辑属性。如果某个值满足该逻辑属性，则该值属于特定类。

定义一个类型(Defining a class)

要定义一个类，你可以这样写：

1. 关键字class
2. 类的名称。这是一个标识符 以大写字母开头。
3. 改类通过extends和/或instanceof关联父类型(supertypes)。
4. 类的主体，用括号括起来。

定义类的格式，例如：

class ClassName [extends Parent] {
      // ...
}

类名首字母必须是大写⚠️，例如：

class OneTwoThree extends int {
  OneTwoThree() { // characteristic predicate
    this = 1 or this = 2 or this = 3
  }

  string getAString() { // member predicate
    result = "One, two or three: " + this.toString()
  }

  predicate isEven() { // member predicate
    this = 2
  }
}

这定义了一个类OneTwoThree，它包含值1,2和3。 特征谓词捕捉 “是整数 1、2 或 3 之一” 的逻辑属性。

OneTwoThree扩展了int，也就是说，它是int的子类型。QL中的类必须始终具有至少一个父类型(supertypes)。使用extends关键字引用的父类型称为类的基类型(base types)。类的值包含在父类型的交集中（即，它们位于类的域类型中）。类从其基类型继承所有成员谓词。

一个类可以扩展多种类型。更多信息，请参阅" 多重继承 "。一个类可以扩展final类型（或final类型的别名），请参阅"final 扩展 “。类还可以特化其他类型，而无需通过instanceof扩展类接口，请参阅” 不扩展子类型 "。

在CodeQL中，类允许多重继承，但是以下操作是非法的:

• 不能继承本身
• 不能继承final类
• 不能继承不兼容的类型，请参考" 类型兼容性 "。

你也可以为类添加注解。可以查看类的注解列表。

类主体(Class bodies)

类的主体可以包含：

• 特征谓词(characteristic predicate)声明。
• 特征谓词(member predicate)声明。
• 任意数量的字段(field)声明。

当你定义一个类时，该类还会从其父类型继承所有非私有成员谓词和字段。

根据它们是否是final的，你可以重写(override)或 隐藏(shadow)这些谓词和字段以赋予它们更具体的定义。

特征谓词(Characteristic predicate)

类似于其他语言中类的构造函数，只能定义一个，我们可以在特征谓词中使用this来限制类中可能的值。在上述例子中，OneTwoThree被限制为1-3中的整数。

成员谓词(Member predicate)

这些谓词仅适用于类中。我们可以这样去调用类的成员谓词：

class OneTwoThree extends int {
    OneTwoThree() { // characteristic predicate
      this = 1 or this = 2 or this = 3
    }
  
    string getAString() { // member predicate
      result = "One, two or three: " + this.toString()
    }
  
    predicate isEven() { // member predicate
      this = 2
    }
}

select 1.(OneTwoThree).getAString()

结果为：

表达式（OneTwoThree)是一个强制类型转换 。它确保1具有类型OneTwoThree而不仅仅是int。因此，它可以访问成员谓词getAString()。

还可以这样调用，例如，你可以使用string定义的内置函数toUpperCase()：

select 1.(OneTwoThree).getAString().toUpperCase()

字段(Field)

这些是在类主体中声明的变量。类主体中可以有任意数量的字段声明。你可以在类内部的谓词声明中使用这些变量。与变量 this 类似，字段必须在特征谓词 中受到约束。

一个简单的例子如下，它输出10以内每个数字的除数：

class SmallInt extends int {
    SmallInt() { this = [1 .. 10] }
  }
  
  class DivisibleInt extends SmallInt {
    SmallInt divisor;   // declaration of the field `divisor`
    DivisibleInt() { this % divisor = 0 }
  
    SmallInt getADivisor() { result = divisor }
  }
  
  from DivisibleInt i
  select i, i.getADivisor()
  

输出的结果如下：

具体类(Concrete classes)

上述所提到的类都是具体的类，具体类是通过限制较大类型中的值来定义的。

抽象类(Abstract classes)

带有 abstract 注释的类称为抽象类。具体而言，对于抽象类中的值，它必须满足类本身的特征谓词和子类的特征谓词。请注意，在这种情况下， final 扩展不被视为子类。

如果您想将多个现有类归类到一个通用名称下，抽象类就非常有用。然后，您可以在所有这些类上定义成员谓词。你还可以扩展预定义的抽象类：例如，如果你导入一个包含抽象类的库，则可以为其添加更多子类。

例子：

希望识别所有可解释为 SQL 查询的表达式。您可以使用以下抽象类来描述这些表达式：

abstract class SqlExpr extends Expr {
  ...
}

现在定义各种子类——每种数据库管理系统对应一个。例如，您可以定义一个子类 class PostgresSqlExpr extends SqlExpr ，它包含传递给执行数据库查询的Postgres API的表达式。你也可以为MySQL和其他数据库管理系统定义类似的子类。

重写成员谓词(Overriding member predicates)

如果一个类从非final 的父类型继承了成员谓词，则可以重写继承的定义。为此，你可以定义一个与继承谓词具有相同名称和属性的成员谓词，并添加 override 注解 。

例如，扩展了一下前面的例子：

OneTwo的getAstring()覆盖了原来的OneTwoThree的getAstring()。

class OneTwoThree extends int {
    OneTwoThree() { // characteristic predicate
      this = 1 or this = 2 or this = 3
    }
  
    string getAString() { // member predicate
      result = "One, two or three: " + this.toString()
    }
  
    predicate isEven() { // member predicate
      this = 2
    }
  }
  
class OneTwo extends OneTwoThree {
    OneTwo() {
      this = 1 or this = 2
    }
    override string getAString() {
      result = "One or two: " + this.toString()
    }
}
from OneTwoThree o select o, o.getAString()

输出的结果如下：

再加一个TwoThree，继续重写getAString()。

class OneTwoThree extends int {
  OneTwoThree() { // characteristic predicate
    this = 1 or this = 2 or this = 3
  }

  string getAString() { // member predicate
    result = "One, two or three: " + this.toString()
  }

  predicate isEven() { // member predicate
    this = 2
  }
}
  
class OneTwo extends OneTwoThree {
  OneTwo() {
    this = 1 or this = 2
  }
  override string getAString() {
    result = "One or two: " + this.toString()
  }
}

class TwoThree extends OneTwoThree {
  TwoThree() {
    this = 2 or this = 3
  }
  override string getAString() {
    result = "Two or three: " + this.toString()
  }
}

from OneTwoThree o
select o, o.getAString()

运行输出的结果为：

多重继承(Multiple inheritance)

一个类可以扩展多种类型。在这种情况下，它会继承自所有这些类型。

例如：

class Two extends OneTwo, TwoThree {}

这个类Two同时继承了OneTwo和TwoThree，它还间接继承自OneTwoThree和int，那么通过特征谓词我们知道其值只能是2。
如果一个子类继承了同一个谓词的多个定义，那么该类还需要手动重写该谓词以避免歧义，在这种情况下我们可以考虑使用super表达式。

例如:

class Two extends OneTwo, TwoThree {
  override string getAString() {
    result = TwoThree.super.getAString()
  }
}

Final拓展(Final extensions)

类可以扩展final类型或final类型的别名。在这种情况下，它会继承这些父类型的所有成员谓词和字段的final版本。通过final扩展继承的成员谓词无法被覆盖，但可以被隐藏。

例如：

class OneTwoThree extends int {
    OneTwoThree() { // characteristic predicate
      this = 1 or this = 2 or this = 3
    }
  
    string getAString() { // member predicate
      result = "One, two or three: " + this.toString()
    }
  
    predicate isEven() { // member predicate
      this = 2
    }
}

final class FinalOneTwoThree = OneTwoThree;

class OneTwoFinalExtension extends FinalOneTwoThree {
  OneTwoFinalExtension() {
    this = 1 or this = 2
  }

  string getAString() {
    result = "One or two: " + this.toString()
  }
}
from OneTwoThree o 
select o, o.getAString()
//from OneTwoFinalExtension o 
//select o, o.getAString()

运行的结果如下：

修改为：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

变量声明出现在不同的上下文中，例如在选择子句中、在量化公式中、作为谓词的参数等等。

从概念上讲，你可以认为变量保存了其类型允许的所有值，但要受到任何进一步的约束⚠️。

例如，考虑以下选择子句：

from int i
where i in [0 .. 9]
select i

仅根据变量 i 的类型，它可以包含所有整数。然而，它受到公式 i in [0 .. 9] 的限制。因此，select 子句的结果是从0 到9之间的10个数字（含 0 和 9 ）。

另外，请注意⚠️查询会导致编译时错误：

from int i
select i

理论上，它会有无限多个结果，因为变量i的可能值并不受限于有限个。想了解更多，可参阅“ 绑定 ”。

自由变量和绑定变量(Free and bound variables)

变量可以扮演不同的角色。有些变量是自由变量 ，它们的值直接影响使用它们的表达式的值，或者 使用它们的公式是否成立。其他变量被称为绑定变量，它们被限制在特定的值集内。

例子如下：

"hello".indexOf("l")

min(float f | f in [-3 .. 3])

(i + 7) * 3

x.sqrt()

第一个表达式没有任何变量。它查找字符串 "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 分别被赋值的值。换句话说，变量的值会影响表达式的值。这些都是自由变量的例子。

类似地，如果公式包含自由变量，则该公式是否成立取决于分配给这些变量的值。例如：

"hello".indexOf("l") = 1

min(float f | f in [-3 .. 3]) = -3

(i + 7) * 3 instanceof int

exists(float y | x.sqrt() = y)

• 第一个公式不包含任何变量，并且永远不会成立（因为 "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 中的定义。

class A extends int {
  A() { this = 1 }
  int getANumber() { result = 2 }
}

class B extends int {
  B() { this = 1 }
  int getANumber() { result = 3 }
}

class C extends A, B {
  // Need to define `int getANumber()`; otherwise it would be ambiguous
  override int getANumber() {
    result = B.super.getANumber()
  }
}

from C c
select c, c.getANumber()

该查询的结果为：

公式Formulas

公式定义表达式中使用的自由变量之间的逻辑关系。

根据赋予这些自由变量的值，公式可能为真或为假。当公式为真时，我们通常说该公式成立 。

例如，如果将值 9 赋给 x ，公式 x = 4 + 5 成立，但对于其他赋值，公式 x = 4 + 5 不成立。有些公式没有任何自由变量。例如， 1 < 2 始终成立，而 1 > 2 永远不会成立。

下面只介绍个人认为比较特殊的点，其它点较为简单，可参考原文^[10]。

顺序(Order)

要使用这些顺序运算符之一比较两个表达式，每个表达式必须具有一个类型，并且这些类型必须兼容并且 可排序的 。

这些符号为：>、>=、<、<=

例如，公式 "Ann" < "Anne" 和 5 + 6 >= 11 均成立。

注解Annotations

注释是一个字符串，您可以将其直接放置在QL 实体或名称的声明之前。类似于Java语言。

例如，要将模块 M 声明为私有的，您可以使用：

private module M {
    ...
}

请注意，一些注释作用于实体本身，而其他注释作用于实体的特定名称 ：

• 对实体进行操作： abstract 、 cached 、 external 、 transient 、 override 、 pragma 、 language 和 bindingset

• 对名称进行操作： deprecated 、 library 、 private 、 final 和 query

例如，如果你使用 private 注释一个实体，那么只有该特定名称是私有的。你仍然可以使用其他名称（使用 alias ）访问该实体。另一方面，如果您使用 cached 注释一个实体，那么该实体本身将被缓存。

具体的例子：

module M {
  private int foo() { result = 1 }
  predicate bar = foo/0;
}

在这种情况下，查询 select M::foo() 会报错，因为名称 foo 是私有的。查询 select M::bar() 是有效的（返回结果 1 ），因为名称 bar 是可见的，并且它是谓词 foo 的别名。

参考

---

1. https://codeql.github.com/docs/codeql-overview/supported-languages-and-frameworks/ ↩ ↩︎

2. https://paper.seebug.org/1324/ ↩︎

3. https://bbs.kanxue.com/article-20135.htm ↩︎

4. https://github.com/webraybtl/CodeQLpy ↩︎

5. https://github.com/WebGoat/WebGoat ↩︎

6. https://codeql.github.com/docs/ql-language-reference/predicates/ ↩︎

7. https://longlone.top/安全/安全研究/codeql/2.CodeQL语法/ ↩︎

8. https://codeql.github.com/docs/ql-language-reference/queries/# ↩︎

9. https://codeql.github.com/docs/ql-language-reference/expressions/# ↩︎

10. https://codeql.github.com/docs/ql-language-reference/formulas/#formulas ↩︎