在Linux系统中，系统调用究竟是如何工作的

这两者看起来都属于系统调用。它们都是向内核请求程序本身无法获取的信息：当前时间，以及文件描述符的访问权限。

gcc -O0 -o mystery mystery.c
strace ./mystery 2>&1 | grep -c clock_gettime

答案是`0`。

读完这篇文章后，你将会了解从`write()`函数开始到代码在内核中运行的整个过程，明白为什么返回路径会比进入内核的过程更为复杂，以及为什么`clock_gettime()`能够跳过这一整个流程。

目录

• 所需准备

• 从用户空间看系统调用

• 跨越边界

• 进入内核：寻找处理函数

• 返回路径与errno的真相

• 从未发生的系统调用

• 边界成本的影响

• 结论

• 后记

所需准备

你需要一台运行Linux系统的x86-64架构机器，以及`gcc`、`strace`和`objdump`工具。在Debian或Ubuntu系统中，这些工具分别属于`build-essential`包、`strace`包和`binutils`包。此外，你还需要熟悉C语言的编程方式。虽然不需要自己编写过内核代码，但也不需要在这里构建或安装内核。

除了其中一个需要使用`sudo`权限的可选跟踪步骤外，所有操作都可以通过普通用户账户来完成。

关于作用域需要说明两点：首先，本文仅针对**x86-64架构**进行讲解。ARM64架构虽然可以使用不同的指令和寄存器规则来实现相同的功能，但如果在每句话中都同时考虑这两种架构，文章的长度会翻倍，而清晰度则会大大降低。其次，内核的内部实现会随版本更新而发生变化。我在本文中使用的测试环境是**Linux 5.15（Ubuntu 22.04，Intel Core i7-10750H）**，对于那些在新版本内核中有所变化的部分，我会特别标注出来。你可以使用`uname -r`命令来查看自己系统的内核版本。

从用户空间来看，系统调用是什么样的

首先需要纠正一个重要的误解：write() 并不是一个系统调用。它只是C语言库中的一个普通函数而已。这个函数会代表你执行系统调用，而这两者之间的区别正是导致人们对内核理解产生困惑的根源所在。

你可以通过去掉libc库，直接自己编写代码来验证这一点。

在x86-64架构上，系统调用遵循固定的规范：你需要将想要调用的函数编号存储在rax寄存器中，而函数的参数则依次存储在rdi、rsi、rdx、r10、r8和r9这些寄存器中。之后，你只需要执行一条名为syscall的指令即可。

这些编号并不是你需要记住的内容，它们实际上存在于你的机器上的头文件中：

grep -E "__NR_(write|getpid|clock_gettime) " /usr/include/x86_64-linux-gnu/asm/unistd_64.h

以这台机器为例，相关的定义如下：

#define __NR_write 1
#define __NR_getpid 39
#define __NR_clock_gettime 228

因此，write函数的编号是1。下面是直接用手编写的不使用libc包装的代码示例：

static long raw_write(int fd, const void *buf, unsigned long count)
{
    long ret;

    __asm__ volatile (
        "syscall"
        : "=a" (ret)                   /* 结果会存储在rax寄存器中 */
        : "a" (1L),        /* rax = 1，即write函数的编号 */
          "D" ((long)fd),  /* rdi = 第一个参数                  */
          "S" (buf),       /* rsi = 第二个参数                 */
          "d" (count)      /* rdx = 第三个参数                  */
        : "rcx", "r11", "memory"
    );

    return ret;
}

编译并运行这段代码后，输出结果会直接显示在标准输出上，而且整个过程中不会用到libc库的任何功能。

注意最后那一行代码——那些被指定为“会被销毁”的寄存器。添加这一行是为了保证程序的安全性。实际上，这是硬件本身的特性，它也解释了上述规范中的一些奇怪之处。

在x86-64架构上，C语言函数会通过rcx寄存器传递第四个参数，而系统调用则使用r10寄存器来传递这个参数。那些声称“因为这是约定俗成的规范”之类的解释，其实都忽略了真正的根本原因：实际上，syscall指令在执行过程中会覆盖rcx寄存器的内容。因此，即使内核想要接收第四个参数，也无法通过这个途径实现，所以应用程序接口不得不绕过硬件的这种限制来进行设计。

这就是第一个能够说明“系统调用与普通函数调用在本质上是不同的”证据。不同的机制意味着不同的规则，而硬件特性在这一点上起到了决定性的作用。

你可以在编译后的二进制文件中直接看到这条syscall指令。

objdump -d --no-show-raw-insn raw_write | grep -B2 -A2 syscall

指令就在那里：

    118b:mov    -0x28(%rbp),%rdx
    118f:(syscall
    1191:mov    %rax,-0x8(%rbp)

只有三行代码：加载一个寄存器，执行一条指令，然后存储返回的结果。这篇文章中提到的其他所有内容都发生在第二行和第三行之间。

跨越边界

当CPU执行syscall时，它会做出普通跳转命令所无法实现的事情：它会改变处理器的权限等级。你的代码是在x86体系结构中所谓的“第3环”中运行的，而内核代码则运行在“第0环”中。

这条指令按顺序执行三项操作：

1. 它将程序中下一条指令的地址保存到rcx寄存器中。这就是返回地址，也因此rcx寄存器的内容会被修改。

2. 它将CPU的状态标志保存到r11寄存器中。

3. 它从三个特殊的CPU寄存器中读取新的指令指针、代码段地址和栈段地址，并将这些新值存储起来。

第三步才是关键。这个新的指令指针并不是来自你的程序，而是来自一个名为LSTAR的机器专用寄存器，而正是内核在启动过程中将这个寄存器的内容设置好了。

这种设计所依赖的安全机制就在这里：虽然用户空间可以触发这一转换过程，但它无法决定转换后会进入哪个位置。唯一能进入的目标地址是arch/x86/entry/entry_64.S文件中的entry_SYSCALL_64函数。

需要注意的是，这条指令并不会访问中断描述符表，也不会创建异常处理框架。在旧系统中，程序是通过int 0x80这个软件中断机制来进入内核的，但这种方式的效率很低。syscall指令的存在正是因为这种方式值得专门为它设计专门的硬件。

1. swapgs

内核会在GS寄存器中为每台CPU保存一个指针，这样它就能找到自己所需的数据结构。在用户空间程序运行期间，GS寄存器中存储的是用户程序放置的内容；而通过一条swapgs指令，内核就可以将这个地址替换为自己的值。关于这条指令，内核的官方文档描述得相当直白，称它非常容易出错，并警告使用者必须确保其使用方式完全正确。如果操作不当，后果将会非常严重。

2. 栈切换机制

你的栈指针是由程序自行指定的值，因此内核无法信任这个值。内核会保存你的rsp寄存器，然后切换到为该线程分配的内核栈中。

3. 构建pt regs

随后，内核会将你保存的寄存器按特定顺序压入这个新的栈中，从而形成一种名为struct pt_regs的C语言结构体。pt regs实际上就是“被冻结的你进程”的状态描述。任何用于检测已停止进程的调试工具、任何会修改进程上下文的信号处理程序，以及任何系统调用处理程序，都会从这个结构体中读取相关数据。

可能还存在第四个步骤：如果你的CPU存在Meltdown漏洞，内核还会在此时交换页表，因为在这种芯片上，当你的代码正在运行时，内核的内存区域无法被安全地映射出来。

这种交换操作并非毫无代价。正因如此，2018年许多系统调用的执行速度明显变慢了；而且，在使用年限较长的机器上，本文后面提到的一些数据也会出现差异。

你可以检查自己的机器是否受到了这种影响：

cat /sys/devices/system/cpu/vulnerabilities/meltdown

如果你的机器采用的是新一代芯片，那么测试结果会显示“未受影响”，因为这类芯片的硬件已经具备了相应的修复机制；而较旧的笔记本电脑则会显示“缓解措施：PTI”，此时它执行的每一个系统调用都会额外增加一些处理开销。

顺便再看看该目录中的其他文件吧——这些文件其实都在说明这种保护机制可能会带来哪些性能影响。

内核内部：查找相应的处理程序

此时，内核已经在自己的栈上继续运行，而你的寄存器数据也已经被安全地保存了下来。内核会调用一个C语言函数do_syscall_64，并将pt regs结构体以及你通过rax寄存器传递的系统调用编号作为参数传给这个函数。

“调度过程”其实可以用很简洁的语言来描述：内核会首先检查系统调用编号是否在有效范围内，然后将其调整到合适的范围，最后跳转到相应的处理程序中：

if (likely(nr < NR_syscalls)) {
    nr = array_index_nospec(nr, NR_syscalls);
    regs->ax = x64_sys_call(regs, nr);
}

其中有两点需要特别说明。

array_index_nospec是一种针对Spectre漏洞的防护措施。在具有投机执行能力的CPU上，单纯的边界检查是不够可靠的，因为处理器可能会在检查完成之前就访问到内存中超出范围的数据。而array_index_nospec这种机制能够确保索引值始终处于有效范围内，从而避免投机攻击的发生。

x64_sys_call这个函数的相关描述在很多旧资料中都是错误的。那些资料会告诉你，内核是通过访问一个名为sys_call_table的函数指针数组来执行系统调用的。但实际上，从内核6.9版本开始，x64_sys_call已经变成了由编译器生成的、用于直接调用相应处理程序的代码。

原因在于一系列连锁反应。为了降低安全风险而采取的那些措施使得通过函数指针进行间接调用变得代价高昂，因为每次这样的调用都需要经历一次“retpoline”优化过程。

而使用switch语句直接进行调用则可以完全避免这种开销。虽然用于追踪的工具仍然需要使用那个调度表，但执行热点代码时并不会读取该表。在我的5.15内核版本中，那种基于表的调度机制依然存在，而这正是为什么在这样的文章中明确指出内核版本名称如此重要的原因。

处理程序的来源

write函数的处理程序被命名为__x64_sys_write，但在内核源代码中你根本找不到这个名称——它是通过一个宏生成的：

SYSCALL_DEFINE3(write, unsigned int, fd, const char __user *, buf, size_t, count)

SYSCALLdefine3表示“这是一个接受三个参数的系统调用”。这个宏会被展开成两个函数：一个是实际的实现代码，另一个是名为__x64_sys_write的封装函数，该函数接收一个struct pt_regs *类型的参数，并从中提取出真正的函数调用参数。

这种间接调用的设计是有意为之的。内核并不依赖用户空间程序在参数寄存器中留下的数据，而是从自己构建的结构体中获取它所期望的值。这种防御机制与array_index_nospec函数中的安全策略类似，只是应用在了函数调用的层面而已。

你完全不必相信这些解释——内核内置的追踪工具ftrace就可以让你看到处理程序的实际运行过程。

要使用这个工具，你需要以root权限运行shell，而不能使用sudo，因为用于过滤输出信息的代码会引用shell自身的进程ID：

sudo -i
cd /sys/kernel/tracing

echo 0 > tracing_on
echo $$ > set_ftrace_pid              # 只追踪当前这个shell
echo function_graph > current_tracer
echo __x64_sys_write > set_graph_function

echo 1 > tracing_on
echo "trigger a write" > /dev/null    # 我们想要捕捉的调用操作
echo 0 > tracing_on

head -40 trace

如果没有set_ftrace_pid这条命令，那么系统会记录下所有写入操作，而在一个正在运行的桌面系统中，这样的输出量实在太大，根本无法阅读。

以下是在测试系统上运行上述命令后得到的部分输出结果（已经进行了简化处理）：

 9)               |  __x64_sys_write() {
 9)               |    ksys_write() {
 9)               |      __fdget_pos() {
 9)   0.124 us    |        __fget_light();
 9)   0.363 us    |      }
 9)               |      vfs_write() {
 9)               |        rw_verify_area() {
 9)               |          security_file_permission() {
 9)               |            apparmor_file_permission() {
 9)   0.264 us    |              aa_file_perm();
 9)   0.457 us    |            }
 9)   0.644 us    |          }
 9)   0.857 us    |        }
 9)   0.083 us    |        write_null();
 9)               |        __fsnotify_parent() {
 9)   0.107 us    |          fsnotify();
 9)   1.383 us    |        }
 9)   2.813 us    |      }
 9)   3.449 us    |    }
 9)   3.720 us    |  }

从外向内阅读这些代码，就能在二十行中了解整个过程。

__x64_sys_write是生成的封装函数。它会调用真正的实现函数ksys_write，后者会通过__fdget_pos获取文件描述符，然后把任务交给虚拟文件系统层vfs_write，在这一点上，内核就不再关心你正在向什么类型的目标进行写入操作了。

security_file_permission会调用AppArmor，因为这台机器运行的是Ubuntu系统。而在SELinux系统中，则会使用其他的安全模块。无论哪种情况，都会有一个安全模块来决定你是否有权执行这个写操作——每次写入操作都会经过这个检查。

write_null是最终执行的函数，但它其实是偶然存在的：上面的代码是将数据写到了/dev/null，所以实际上就是这个函数在起作用，它的任务就是将你的数据丢弃掉。如果将同样的写操作指向磁盘上的文件，那么就会调用文件系统相关的函数，而上面那些代码就不会被执行了。

整个过程只用了3.7微秒，右边的时间戳可以显示各个步骤的执行耗时。

<完成测试后，需要把跟踪工具重新恢复原状：

echo nop > current_tracer
echo > set_graph_function
echo > set_ftrace_pid

<如果你的系统中没有/sys/kernel/tracing这个目录，可以尝试使用/sys/kernel/debug/tracing代替。

返回路径与errno的真相

<处理函数执行完成后会返回一个数值，这个数值会被存储在rax寄存器中，而你的程序最终得到的也是这个值。

<这就引出了一个很少被直接问到的问题：如果内核只能返回一个数值，那么它该如何同时报告“发生了什么错误”以及“确实发生了错误”这一事实呢？

<答案是：内核并没有专门的通道来传递这些信息。内核会将错误信息以负数的形式存储在同一个寄存器中。例如，成功的24字节写入操作会返回24，而向一个已关闭的文件描述符进行写入操作则会返回-9，因为EBADF就是错误代码9。

<现在再考虑到errno这个变量的存在，就有些地方说不通了。errno是你的进程中的变量，而内核并不会直接修改你的程序变量。

<下面是一个测试例子：将errno设置为0，然后执行一个肯定会失败的原始系统调用，最后比较这两个值：

#include          /* fprintf, stderr */
#include          /* errno */

/* raw_write()是上一节中提到的函数 */

errno = 0;

long ok  = raw_write(1, "written via raw syscall\n", 24);
long bad = raw_write(999, "x", 1);          /* 文件描述符未打开 */

fprintf(stderr, "ok = %ld\n",  ok);
fprintf(stderr, "bad = %ld\n", bad);
fprintf(stderr, "errno = %d\n", errno);

<运行这个程序，你就能看到结果了。

通过原始系统调用实现  
ok = 24  
bad = -9  
errno = 0  

结果就是这样：内核返回了 -9，而 errno 的值也没有发生变化。

errno 实际上是 libc 规定添加的一个机制。当你调用普通的 write() 函数时，该函数的封装层会检查返回值是否是一个较小的负数；如果是的话，就会将这个值取反，然后将其存储到 errno 中，并向你返回 -1。每个 C 程序员都熟悉这种“返回 -1 并检查 errno”的机制，但实际上这种做法完全是在用户空间中形成的约定，而内核本身的工作方式与此截然不同。

一旦了解了这一点，某些常见的错误现象就会变得更容易理解了。errno 只有在调用失败之后才有意义，因为它只不过是最后一个出错的函数封装层所写入的一个变量而已。

两种返回用户空间的方式

回到用户空间有两种途径：一种速度较快，另一种则较慢。

速度较快的方式是使用 sysret，它与 syscall 的功能类似：它会将你的指令指针从 rcx 中恢复出来，将标志位从 r11 中读取出来，然后在几个时钟周期内使程序返回到第 3 核心层。

速度较慢的方式是使用 iret，这是一种用于从中断中恢复执行的通用指令。它的执行速度明显更慢，而内核只有在无法信任 sysret 时才会使用它。进入代码中的注释也解释了原因：由于 AMD 和 Intel 处理器都存在某些缺陷，sysret 在处理非标准地址时会遇到问题；因此，每当有可能导致你的程序状态发生改变的情况下，内核都会强制选择更安全的返回方式。通常情况下，通过 ptrace 功能侵入系统并修改寄存器的调试工具就是导致这种情况的罪魁祸首。

在这两种指令被执行之前，内核会先完成一些它之前推迟处理的操作：它会检查是否有未处理的信号需要发送，同时也会判断调度器是否要求重新使用 CPU；如果确实如此，那么你的进程就会停止运行，其他进程则会继续执行。

这意味着系统调用并不仅仅是一种服务请求，它也是让你的进程停止运行的一个重要途径。你本来只是请求写入 5 个字节的数据，但在返回用户空间的过程中，内核会重新评估关于你的程序的诸多信息，甚至会考虑是否应该让你继续执行下去。

那种永远不会发生的系统调用

现在让我们回到开头提到的那个谜题上来。

查看你自己的进程的内存映射吧：

cat /proc/self/maps | tail -4

输出结果的最后部分通常会显示如下内容：

7fff32f97000-7fff32f9b000 r--p  [vvar]  
7fff32f9b000-7fff32f9d000 r-xp  [vdso]  

其中 [vdso] 表示“虚拟动态共享对象”。这是一种体积较小但功能完备的共享库（实际上它是真正的 ELF 格式文件，包含符号表），内核会将其映射到每个进程的内存空间中。因为内核会告诉每个进程这个共享库被放置在了哪个位置，所以你可以自己获取这个共享库的副本并对其进行分析。

#include 
#include       /* getauxval, AT_SYSINFO_EHDR */
#include         /* getpagesize */

int main(void)
{
    void *vdso = (void *)getauxval(AT_SYSINFO_EHDR);   /* 内核会告诉我们这个地址在哪里 */
    size_t len = 2 * getpagesize();                    /* 这次映射占用了两页内存 */

    FILE *f = fopen("vdso.so", "wb");
    fwrite(vdso, 1, len, f);
    fclose(f);

    printf("vDSO被映射到了地址 %p\n", vdso);
    return 0;
}

AT_SYSINFO_EHDR这个宏定义位于文件中。如果省略了这个头文件，编译过程中不会出现警告信息，但编译会直接失败，错误提示会是“AT_SYSINFO_EHDR未定义”。

运行上述程序后，可以像处理其他库一样查看它的符号表：

./dump_vdso && objdump -T vdso.so | grep __vdso

执行后会看到以下内容：

__vdso_gettimeofday
__vdso_clock_gettime
__vdso_clock_getres
__vdso_time
__vdso_getcpu

答案就在这里。clock_gettime这个函数就在列表中。

当调用clock_gettime()函数时，libc会通过vDSO来执行这个功能。这段代码是由内核开发者编写的，并随内核一起发布的，但它是在第3层栈环境中执行的，属于你的进程的一部分。它从[vvar]页面中读取当前时间（这个页面是内核维护的只读页面），然后返回结果。

在整个过程中并没有权限上的变化，也没有使用syscall指令、进行栈切换，或者修改pt_regs结构体。因此，strace工具也无法检测到这一过程，因为strace是通过监控系统调用的边界来工作的，而这个调用根本不会跨越这个边界。

这就是整个原理所在。内核利用了一些那些被频繁调用、不需要特殊权限就能读取数据、并且只会返回内核愿意公开的信息的函数，从而实现了这一目标。

最后提到的这个限制也是为什么列表中的函数数量如此少的原因。write()函数就无法这样使用，因为它会修改属于内核的状态；而获取时间信息这样的操作则不会。因此，时钟信息、当前时间以及CPU编号这些数据可以直接被调用者访问到。

边界成本意味着什么

以上内容都是关于实现机制的描述，现在来看看实际带来的代价是多少。

这个测试用例比较了两种不同的系统调用方式：一种肯定会触发某些限制，另一种则绝对不会。对于第一种情况，使用了syscall(SYS_getpid)函数；而通过syscall()这种封装机制进行的调用，则能够确保真正发生跨层调用。

/* 摘录。需要引入、和头文件，还需要一个名为now()的辅助函数，该函数能以双精度浮点数的形式返回当前时间所对应的秒数，此外还需要上面定义的ITERATIONS常量。 */

double a = now();
for (long i = 0; i < ITERATIONS; i++)
    sink += syscall(SYS_getpid);

double b = now();
for (long i = 0; i < ITERATIONS; i++)
    clock_gettime(CLOCK_MONOTONIC, &ts);

在测试机器上，分别进行了两百万次以下操作：

使用系统调用getpid()：每次调用耗时106.9纳秒
使用vDSO调用clock_gettime()：每次调用耗时17.2纳秒
两者之间的效率比约为6.2倍

效率相差大约六倍，而getpid()已经算是系统调用中效率最高的一种了。它只需要读取一个字段然后返回结果，因此在那107纳秒的耗时中，几乎没有任何时间是用于实际的数据处理工作。实际上，大部分时间都花在了权限切换、堆栈管理以及相关的底层操作上。

不过这里有一个需要注意的地方，因为这个因素比具体的效率数值更为重要。

那107纳秒的耗时其实已经接近最佳情况了。看看这台机器之前报告的结果：对于Meltdown漏洞，它“没有受到影响”，因此根本不会进行页表切换操作；而对于Spectre漏洞，它采用的缓解措施是“Enhanced IBRS”，这种机制是通过芯片本身来实现的，而不是通过软件中的重排指令来处理的。因此，这款CPU规避了两种效率最低的优化步骤。

所以你最好自己运行这个基准测试，并同时查看你的系统所采取的缓解措施相关信息：

grep . /sys/devices/system/cpu/vulnerabilities/*

如果你的系统中显示的缓解措施是“PTI”，那么你的程序在进行跨权限操作时所消耗的时间肯定要比这里测得的结果长得多，因此相应的效率数值也会更低。较旧的芯片型号可能会表现得更加糟糕。

把效率比看作是一个相对稳定的结果，而具体的耗时数值则只是某台机器上的测试结果而已。这个数值会随着你使用的CPU、内核版本以及所采取的缓解措施的不同而有所变化。建议多运行几次测试来获得更准确的结果。在我使用的这款笔记本电脑上，多次测试得到的结果之间的差异约为15%，这个数据可以让你了解单个测试结果的可靠性。

grep . /sys/devices/system/cpu/vulnerabilities/*

同一组测试还得出了一个能够纠正一些普遍误解的结果：通过普通的libc库来调用getpid()所消耗的时间，与直接使用原始的syscall(SYS_getpid)所消耗的时间是一样的。原来glibc库会缓存进程ID以避免重复进行这种系统调用，但几年前就已经停止了这种做法，因为在进行fork操作或命名空间变更时，保持缓存数据的准确性反而会比多花费100纳秒的代价更糟糕。

“效率相差六倍”这个数字听起来可能比较抽象，但当你将其应用到具体的场景中时，就会明白它的意义了。例如，一个程序如果执行一百万次小的read()操作，那么其中大约有十分之一的时间都会被用于跨权限操作。正是这种压力促使现代内核接口设计出现了许多优化措施：比如io_uring机制的存在，使得提交一千个I/O操作只需要进行一次跨权限操作而已，而不是原来的每一项操作都需要单独处理。批量执行系统调用、缓冲写入数据，以及使用sendfile()代替循环读写操作，这些都属于同样的优化思路：并不是为了减少工作量，而是为了减少跨权限操作的次数。

结论

现在，你可以完整地追踪一个系统调用的整个过程。你已经在自己的二进制文件中看到了syscall指令，观察到当文件描述符出错时，其返回值会是-9，而errno的值却保持为零；你还从自己的地址空间中提取出了vDSO，并读取了它的符号表，同时还测量了自己CPU在执行这些操作时所消耗的时间。

更重要的是，你现在已经建立起了一个实用的知识模型。当你看到io_uring能够减少系统调用的开销时，你就清楚地知道“开销”到底意味着什么；当分析工具显示某个函数的执行时间属于entry_sySCALL_64阶段时，你就会明白这个函数的具体功能；而当strace无法检测到任何相关信息时，你就会知道应该先检查vDSO，而不是怀疑这个分析工具本身的准确性。

今后还有几个方向可以探索。你可以运行ftrace工具，追踪__x64_sys_write这个系统调用到底是如何进入文件系统的；也可以阅读arch/x86/entry/entry_64.S这份文档——尽管它被标注为“难度较高”，但实际上比人们想象的要容易理解得多。或者，在较老的机器上查看/sys/devices/system/cpu/vulnerabilities/目录，了解各种安全措施在实际应用中会带来多少性能损耗。

后记

目前我正在尝试在Linux内核的基础上设计一种新的操作系统，这种系统会将Android风格的权限和功能模型引入桌面操作系统中，同时确保其与Debian生态系统的完全兼容性。这项研究最近产生了一些非常有趣的结果，而这篇文章也正是这些研究的成果。

在继续研究形式化验证技术之前，我还会继续深入探讨Linux内核的相关内容。形式化验证技术在DO-178C和DO-333等标准中有着重要的应用，因为在航空电子软件领域，用于检测这些软件的工具本身也需要经过严格的验证。通常来说，这些验证工具包括Viper、Why3以及Z3等工具。

与此同时，我也会在thechris.in这个平台上撰写关于那些需要在现实环境中运行的系统的文章。其中就包括一篇与这篇文章相关的文章，探讨了在那种“成本可测但肉眼无法看见”的抽象层上进行开发所带来的挑战。