Posted 2023-06-09Updated 2023-11-275 minutes read (About 689 words)

get the function offset and jump to the function at runtime dynamically

Indeed, getting the function offset dynamically during runtime would require you to parse the symbol table of the binary. This is a complex task that would usually be done using a library like libelf or libbfd.

However, if you want a simpler solution that uses command-line tools, you can use nm or readelf to create a text file with the function offsets, and then read that file at runtime. Here’s how you might do it:

Compile your program with debug symbols and without ASLR:
1
gcc -g -fno-pie -no-pie myprogram.c -o myprogram
Create a text file with the function offsets:
1
nm myprogram | grep ' T ' > offsets.txt
This command will create a text file called offsets.txt that contains the offsets of all the functions in myprogram. The ‘T’ indicates that we are interested in the text (code) section of the binary.
Read the offsets file at runtime and create function pointers:

Here’s an example in C that reads the offsets file and creates a function pointer for my_function:

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <string.h>

void my_function() {
    printf("Hello, world!\n");
}

int main() {
    FILE *file = fopen("offsets.txt", "r");
    if (file == NULL) {
        printf("Cannot open offsets file!\n");
        return 1;
    }

    uintptr_t offset = 0;
    char name[256];

    while (fscanf(file, "%lx %*s %255s", &offset, name) == 2) {
        if (strcmp(name, "my_function") == 0) {
            break;
        }
    }

    fclose(file);

    if (strcmp(name, "my_function") != 0) {
        printf("Did not find my_function!\n");
        return 1;
    }

    // Cast the offset to a function pointer
    void (*func_ptr)() = (void (*)())offset;

    // Call the function through the pointer
    func_ptr();

    return 0;
}

This program reads the offsets file, line by line, until it finds my_function. It then creates a function pointer using the offset and calls the function.

Note that this only works if your program is compiled without ASLR (hence the -no-pie flag to gcc). If ASLR is enabled, the offsets will be different every time the program is run. Also note that this example only works for function with no parameters, if your function has parameters, you need to adjust the function pointer type accordingly.

Please be aware that parsing the symbol table and manually creating function pointers like this is risky and not generally recommended. It can easily lead to crashes, undefined behavior, or security vulnerabilities if not done properly. Use it carefully and only if you understand exactly what you are doing.

dlsym

It’s indeed unusual and more complex to dynamically determine the offset and execute a function at runtime. For this, you would need to parse the binary’s symbol table at runtime. Here’s a rough idea of how you might do it using the dlfcn library’s dlsym function, which can find a function’s address in a dynamically linked executable at runtime:

#include <stdio.h>
#include <dlfcn.h>

void my_function() {
    printf("Hello, world!\n");
}

int main() {
    void* handle = dlopen(NULL, RTLD_LAZY); // Open the current executable
    if (!handle) {
        fprintf(stderr, "%s\n", dlerror());
        return 1;
    }

    dlerror(); // Clear any existing error

    // Find the function in the executable's symbol table
    void (*func_ptr)() = dlsym(handle, "my_function");

    char* error = dlerror();
    if (error) {
        fprintf(stderr, "%s\n", error);
        return 1;
    }

    // Call the function through the pointer
    func_ptr();

    dlclose(handle); // Close the executable

    return 0;
}

This example uses the dlopen function to open the current executable (the NULL argument means to open the current process’s symbol table), the dlsym function to find the function in the symbol table, and a function pointer to call the function.

This approach requires that your executable is dynamically linked and the function is exposed in the symbol table, i.e., it’s not declared as static and not stripped out by the linker or strip tool. You may need to pass the -rdynamic option to the linker (usually via -Wl,-export-dynamic gcc option) to ensure that the symbol is included in the dynamic symbol table.

Again, manipulating function pointers like this can be dangerous and is generally not recommended unless you know what you are doing. The best way to call a function at runtime is typically to use a function pointer that is set at compile time.

Posted 2023-05-30Updated 2023-11-274 hours read (About 34828 words)

毕业论文（设计）: 基于 WebAssembly 的云原生时空数据分析技术研究：以 GPlates 为例

Github repo: https://github.com/yunwei37/gplates-wasm

摘要（中文）

云计算的发展为基于 Web 的时空数据分析应用带来了诸如弹性伸缩、高可用性等优势，但传统的以容器方式部署的云端 Serverful 应用资源占用较高、部署运维不够便捷，同时在 WebGIS 中应对较大规模数据处理、高计算能力要求以及复杂图层渲染等需求时仍面临重大挑战。WebAssembly（Wasm）作为一种可以在浏览器中运行的跨平台低级虚拟机和指令格式，可显著提高Web应用的计算性能和渲染效率，同时也可在云端运行，作为无服务器计算冷启动问题的解决方案。GPlates 是一款C++ 编写的开源桌面端交互式板块重建与分析应用，可实现交互式操作板块构造重建和地质时间的可视化，具有广泛的应用场景。本论文针对时空数据分析的挑战，提出了一种基于Wasm的解决策略，并以GPlates软件为例进行了实证研究。

首先，本论文探讨了基于Wasm的Web时空数据分析与可视化技术，对GPlates软件中的板块构造重建和GIS空间分析等关键功能模块进行了拆分与重构，成功将其移植到云端和浏览器中的Wasm平台上，实现了GPlates的前端开发库和 WebGIS 应用，为 Web 应用提供了更完备的 GPlates 功能的同时也大幅度提升了其前端计算和渲染的性能。测试表明，对于计算密集型的应用，Wasm在某些情况下可为前端带来接近 50% 的性能提升，并且可获取接近服务端执行 C++ 代码的性能。

关键词： WebGIS；WebAssembly；时空数据分析；无服务器架构；GPlates；云原生；

Abstract （英文）

The evolution of cloud computing has brought about advantages such as elastic scalability and high availability to web-based spatio-temporal data analysis applications. However, traditional cloud Serverful applications deployed via containers consume significant resources and lack operational convenience. Additionally, major challenges are faced when addressing requirements such as large-scale data processing, high computational capacity, and complex layer rendering within WebGIS. As a cross-platform, low-level virtual machine and instruction format that runs in the browser, WebAssembly (Wasm) significantly enhances the computational performance and rendering efficiency of web applications and also runs in the cloud, presenting a solution to the cold start issue of serverless computing. GPlates, an open-source desktop application for interactive plate tectonic reconstruction and analysis written in C++, allows for the visualization of geologic time and interactive plate tectonic reconstruction, and has broad application scenarios. This paper proposes a Wasm-based solution to the challenges of spatio-temporal data analysis, with empirical research conducted using the GPlates software as an example.

Initially, this paper investigates web spatio-temporal data analysis and visualization technologies based on Wasm. It disassembles and rebuilds key function modules such as plate tectonic reconstruction and GIS spatial analysis in GPlates software. This has been successfully ported to the Wasm platform in the cloud and browser, resulting in a front-end development library for GPlates and a WebGIS application. This not only provides more comprehensive GPlates functionalities for web applications but also significantly improves their front-end computation and rendering performance. Tests indicate that for computation-intensive applications, Wasm can offer up to 50% performance improvement on the front end in certain cases, with performance almost equivalent to running C++ code on the server-side.

The paper also utilizes the Wasm ecosystem to construct a cloud-native application example for GPlates’ web application. Adopting the serverless architecture concept, the corresponding GPlates WebGIS application has been deployed on Amazon Web Services (AWS) in the form of Wasm functions-as-a-service. Results demonstrate that this deployment approach not only substantially enhances operational efficiency and reduces deployment costs but also features automatic scalability in the face of load variations.

Keywords:** cloud-native, spatiotemporal data analysis, WebAssembly, GPlates, serverless GIS framework, large language models**

绪论

1.1 研究背景与意义

随着社会经济的不断发展，地球科学领域对时空数据分析的需求日益增长。时空数据分析已成为地质与古地理重建等领域的关键技术，对于研究盆地演化，造山运动，深部资源勘探，古生物，古海洋和古气候等均具有重要意义。同时，伴随着云计算和大数据技术的快速发展，云原生技术也正逐渐成为时空数据分析的新兴应用平台，其弹性伸缩、高可用性等特性使得云原生时空数据分析在处理海量数据和应对高负载场景时具有明显优势。

尽管云原生技术为时空数据分析带来了诸多优势，但其在实际应用中仍面临着一系列挑战。首先，时空大数据具有数据量大、计算能力要求高的特点，传统的 WebGIS 在处理相对大规模的数据时，由于 JavaScript 的计算性能限制，可能导致前端计算的性能瓶颈，将数据传输到后端进行处理又较为消耗后端的计算资源，也会带来网络传输的性能开销；其次，在复杂图层渲染方面，如何快速呈现海量数据，并实现高效的可视化交互，也对现有的 WebGIS 技术栈提出了更高的要求。此外，如何保障云原生环境下、尤其是以 SaaS （Software as a service，软件即服务）方式提供服务的 GIS 应用的数据安全性和隐私保护能力，也是一个亟待解决的问题。WebAssembly 作为一种在浏览器中的跨平台低级虚拟机和高性能指令格式，能够显著提高 Web 应用的计算性能和渲染效率，因此利用 WebAssembly 技术在网页前端进行时空数据分析和渲染，具有很大的研究价值和实际应用前景。

另一方面，云计算中的无服务器架构也为时空数据分析提供了新的解决思路。无服务器计算（Serverless），又称函数计算（Function as a Service, FaaS），是一种新型计算模式，完全依赖于云平台，旨在让云平台接管应用服务的部署、监控、扩容、容错等工作。通过将计算任务分布在多个云端函数上，无服务器架构可以在高负载场景下自动扩缩容，以满足不断变化的计算需求。同时，通过按需付费的计费模式，无服务器架构有助于降低资源使用成本。然而，无服务器架构在应用于时空数据分析时，也面临着一些挑战。例如，如何解决云函数之间的数据传输和通信问题，以保证时空数据分析任务的高效执行；如何处理大量并发请求时产生的云函数冷启动问题，以避免对响应时间造成不良影响等。

为解决上述挑战，本论文提出了一种基于 WebAssembly（Wasm）的解决方案。WebAssembly 作为一种在浏览器中的跨平台低级虚拟机和指令格式，能够显著提高Web应用的计算性能和渲染效率，同时 WebAssembly 也可以在云环境下直接执行，很大程度上能缓解无服务器架构的云函数冷启动问题。结合无服务器架构，基于 WebAssembly 的时空数据分析方案将有效提高数据处理能力、降低延迟，并优化资源利用。

GPlates 是一个开源的板块构造地理信息系统，可实现交互式操作板块构造重建和地质时间的可视化，被广泛应用于构造学，地球动力学，盆地演化，造山运动，深部资源勘探，古生物学，古海洋学和古气候学等领域。

本论文旨在探讨基于 WebAssembly 的 WebGIS 时空数据分析与可视化技术，并对比其与传统 JavaScript 方案在计算性能和内存管理方面的优劣。此外，本论文将以 GPlates 软件为例，对其板块构造重建和 GIS空间分析功能等模块进行拆分与重构，以便将其成功移植到浏览器和云端的 WebAssembly 平台上，从而实现一种基于 WebGIS 的 GPlates 服务。这种服务具有更高的计算性能和可扩展性，可广泛应用于云原生时空数据分析领域。

本论文希望借助 WebAssembly 生态，为 GPlates Web 应用构建一个完整的应用示例，因此还探讨了云原生无服务器 GIS 框架的开发和应用。本论文采用无服务器架构思想，在亚马逊网络服务（AWS）上，以云原生函数即服务的方式实现并部署了相应的 GPlates WebGIS 应用。这种部署方式相对于传统的以虚拟机或容器化方式部署的云服务，不仅可以大大提高系统的运维效率和降低部署成本，还能在高负载情况下更高效地实现自动扩缩容功能，从而满足时空数据分析在大规模数据处理和高计算能力需求方面的挑战。

综上所述，本论文具有重要的理论和实践意义,将进一步推动云原生时空数据分析技术的创新与发展，并为地球科学、城市规划和环境监测等领域提供了一定的参考价值。

1.2 国内外研究现状

地理信息系统（Geographic Information Systems，GIS）自20世纪70年代诞生以来，已经经历了数十年的发展历程，并从最初的计算机辅助制图技术，逐渐演变为建立在云计算和大数据之上的地理信息服务。GIS 技术已经渗透到智慧城市、资源环境、交通运输、商业金融等众多领域。

云计算与时空数据分析研究现状

云计算作为一种新兴的计算模式，已经引起了众多研究者的关注。自2006年亚马逊推出 Elastic Compute Cloud（EC2）以来[1]，云计算在各个领域得到了广泛应用，包括地理信息科学领域。2011年云 GIS 的概念被提出，相比于传统 GIS 系统，云 GIS 具有伸缩性、高可用性和按需付费等优势[2]。随后，许多学者开始研究云计算与 GIS 的结合，并在各种应用场景中实现基于云的时空数据分析[3]。同时，SaaS（Software as a Service）模式作为一种将 GIS 应用部署在云端的解决方案，也逐渐得到了推广和应用。

随着云计算与大数据技术的融合，Serverless 架构被提出并逐步受到应用。Serverless 是一种无服务器架构模式，使开发者能够将更多关注点放在业务逻辑实现上，而无需关注底层资源和硬件管理。其特征可以归纳为：资源的解耦和服务化、自动弹性伸缩、按使用量计费等；相应带来的优势有：低运维、低成本、高弹性、高可用等。2015年，AWS（Amazon Web Services）推出了名为 AWS Lambda 的云函数服务，引发了业界对无服务器计算的广泛关注[4]。通过 Lambda，用户只需关注应用程序的代码逻辑，无需考虑扩展、部署、容错、监控以及日志记录服务器配置等问题，因而又称之为”无服务器”计算。

随着无服务器计算逐渐成为主流，越来越多的应用开始采用这种计算方式，因为它可以更便宜、快速且按需扩展大量实例。对于传统的 SaaS 架构，可以将系统内用户最希望定制的功能进行梳理、拆分、抽离，再基于 Serverless工作流重构 SaaS 系统，结合函数计算提供无状态能力，并重新编排这些功能点，从而实现不同的业务流程。

与此同时，WebAssembly（Wasm）作为一种可以在浏览器中执行的虚拟机和指令集，也引起了学界与业界更多的关注和探讨。尽管 Wasm 最初是为了提高网页中性能敏感模块的表现而提出的字节码标准，但它不仅能用在浏览器中，还可以用在其他环境中。WebAssembly 越来越多地用于难以部署 Linux 容器或应用程序性能至关重要的边缘计算场景，以及作为一种针对无服务系统的潜在解决方案[5]。Serverless 强依赖高度优化的冷启动，Wasm 运行时（如 WasmEdge）非常适合为下一代无服务器平台提供动力[6]。SecondState、Cloudflare、Netlify 和 Vercel 等著名公司都支持通过其边缘运行时部署 WebAssembly 功能[7]。其他许多企业，如 Grafbase 正在使用 Wasm，使开发者能够在边缘用他们选择的语言编写和部署 GraphQL 解析器[8]。Wasm 已经改变了无服务器环境的潜力，凭借近乎即时的启动时间、较小的二进制文件大小以及平台和架构的中立性，Wasm 二进制文件可以用运行当今无服务器基础设施所需资源的一小部分来执行。本论文会在下一章节中，详细讨论关于 WebAssembly 的技术发展现状。

WebGIS 与 WebAssembly 技术研究现状

WebGIS 是一种将地理信息系统（GIS）应用于互联网环境的技术，它允许用户通过网络浏览器访问和操作地理数据，具有数据共享、互操作性和易用性等优势。WebGIS的发展使得地理信息不再局限于专业人士，普通用户也可以轻松获取和分析地理数据。随着云计算技术的发展，WebGIS 技术与云原生和软件即服务（SaaS）的结合可以使 GIS 应用更加高效、易用和可扩展。云原生技术可以为 WebGIS 提供弹性伸缩、高可用性等特性，实现地理数据和计算资源的集中管理和按需分配；SaaS 模式将 GIS 功能以服务的形式提供给用户，使得 GIS 的部署和维护变得更加简便。用户无需购买和安装复杂的软件，仅需通过网络浏览器连接即可使用 GIS 功能，可以在任何有互联网连接的区域和设备中，进行地理信息检索、时空数据分析与可视化等操作。

WebGIS 的发展历程与地理信息系统、数字地图和互联网的发展密切相关。1993 年，第一个实现分布式地图生成的主要 Web 映射程序问世。这款名为 PARC Map Viewer的软件具备动态用户地图生成功能，取代了静态图像，并允许用户在无需本地安装的情况下使用 GIS。Esri 作为 GIS 行业的领导者之一，在 2014 年推出了具备关键 WebGIS 功能的 ArcGIS Online[9]。

有大量研究已经关注到 WebGIS 与云计算和 SaaS 的结合。例如， Agrawal 等[10]综述了基于 SaaS 的 WebGIS 系统，使非专业用户可以方便地利用 GIS 功能进行数据分析。还有一些商业应用，如 CartoDB 和 Mapbox，已经将 WebGIS 与云计算和 SaaS 模式相结合，提供了易于使用、高性能的地理信息服务。GPlates 作为一个开源的板块构造地理信息系统，它的开发团队也在 Web 端为用户提供了 3D 地球物理和地质数据可视化、交互式板块构造重建、地表动态地形等功能，同时也作为 GPlates Web Service 网络服务，以容器的形式发布并可一键部署到云端[11]，这进一步丰富了其应用领域，为地球科学研究带来了重要贡献。

近年来，WebAssembly（Wasm）[12]作为一种可以在浏览器中高效执行的跨平台的低级虚拟机和指令集，逐渐成为 Web 技术发展的新趋势。WebAssembly 的出现旨在解决传统 JavaScript 在高性能计算和复杂图形渲染方面的局限性，同时也可以作为一种将桌面端应用移植到 Web 平台发布的方案。

WebAssembly 的历史可追溯到 2015 年[13]，由 Mozilla、Google、Microsoft 和 Apple 四大浏览器厂商联合推出，其目的是为了解决传统 JavaScript 对于高性能计算的局限性。2017 年，WebAssembly 1.0 标准正式发布，得到主流浏览器的支持[14]。基于 Wasm 的研究在 WebGIS 领域已经取得了一定进展，但相对来说还不普遍。例如，Kolak 等人的研究利用 WebGIS 和 WebAssembly 技术开发了一个名为”US COVID Atlas”的系统，可以实时监测和探索性分析新冠疫情下的县级指标[15]，该研究实现的编译到 WebAssembly 的开源空间中间件组件(libgeoda)也为 WebGIS 的发展提供了新思路和方法。这些技术和应用对于时空数据分析的发展具有重要的意义，也为今后相关领域的研究提供了新的思路和方法。

另一方面，Wasm 也为复杂的地理数据处理和分析提供了新的可能性。例如，基于 Wasm 的空间分析算法可以在客户端执行，并减轻服务器端的计算负载。许多知名企业也开始将其应用于其 GIS 平台以提高性能和效率，例如，Cesium 是一家专注于三维地理信息可视化的公司，其开源产品 CesiumJS 已经引入了 Wasm 技术以实现更高效的三维地形加载和渲染[16]、更快速的地理数据处理等效果。此外，超图软件作为一家国内领先的地理信息软件提供商，据相关报道[17]，也正在探索将 Wasm 技术应用于其产品线，以优化其 WebGIS 产品的性能表现，实现更高效的地理数据处理、分析和地图渲染等功能。

综上所述，WebGIS 与云计算的结合，以及 Wasm 技术的发展为时空数据分析与 WebGIS 等领域带来了崭新的机遇。这些技术的进一步研究和应用可能可以对地理信息科学领域的工程实践产生深远影响。

1.3 论文研究内容

本论文研究内容主要围绕云原生时空数据分析技术展开，结合 WebAssembly（Wasm）和 GPlates 软件进行实证研究，并在此基础上编写对应章节。具体的主要工作内容及成果如下：

（1）基于 WebAssembly 的 Web 时空数据分析与可视化技术。本论文详细探讨了 Wasm 技术在 Web 时空数据分析和可视化方面的应用，并通过对比实验验证了 Wasm 相较于传统 JavaScript 方案在计算性能和内存管理等方面的显著优势。本论文将详细介绍 Wasm 技术的基本原理、特性以及在时空数据分析中的应用场景。

（2）GPlates 软件的关键功能模块拆分与重构。为了将 GPlates 软件移植到 Wasm 平台，本论文对其板块构造重建和 GIS 空间分析等关键功能模块进行了细致分析、拆分、重构与移植，实现了一种基于WebGIS 的 GPlates 服务，并详细描述了这一过程中遇到的挑战和解决方案。

（3）云原生无服务器 GIS 应用示例设计与实现。为了为 GPlates Web 应用构建一个完整的云原生应用示例，将 WebAssembly 模块在云端运行，本论文设计并实现了一个云原生无服务器 GIS 框架，并采用无服务器架构思想，在亚马逊网络服务（AWS）上部署了相应的 GPlates WebGIS 应用。本论文将详细讨论无服务器 GIS 应用的设计理念、架构及关键技术，并通过研究验证了该框架在提高运维效率、降低部署成本以及实现自动扩缩容等方面的优势。

通过以上研究内容，本论文为云原生时空数据分析技术的发展探索了新的理论和实践基础，为相关领域提供了有益的参考。在后续章节中，本论文将分别对上述三个研究内容进行详细论述，并展示实证研究的成果。

1.4 论文章节安排

本论文分为六个章节，各章的安排如下：

第一章：绪论。首先对所要研究课题进行背景调查和意义概述，然后对云计算、大数据和时空数据分析的发展现状进行介绍，分析当前云原生时空数据分析中遇到的难点和关键技术，最后介绍本论文的主要工作。

第二章：相关技术介绍和分析。首先介绍云计算、大数据和时空数据分析的背景知识，然后介绍 WebGIS 技术的发展与挑战，接着介绍 WebAssembly 技术，和基于 WebAssembly 的时空数据分析与可视化技术。本论文将首先对Wasm在时空数据分析中的应用进行介绍，然后设计并实施 Wasm 与传统JavaScript 方案的性能对比实验，分析实验结果并讨论 Wasm 在时空数据分析和可视化方面的优势。

第三章：GPlates 软件的拆分与重构。为了将 GPlates 在浏览器端和云端的WebAssembly 虚拟机中部署，首先要将 GPlates 迁移到 WebAssembly 平台。本章首先简要介绍GPlates软件及其核心算法，然后对GPlates软件进行分析和研究，接着对板块构造重建与GIS空间分析等功能模块进行拆分与重构，最后分析、测试重构后的各功能模块在Wasm平台上的实现正确性，与性能表现。

第四章：基于 WebGIS 的云原生 GPlates 服务实现。首先设计并构建云原生无服务器 GIS 框架，接着在亚马逊网络服务（AWS）上部署相应的 GPlates WebAssembly 应用，最后对部署结果进行测试并分析系统性能。

第五章：结论与展望。首先总结本论文的研究结论，然后分析研究中存在的不足，最后展望未来研究方向和可能的技术发展趋势。

3 GPlates软件的重构与迁移

在地球科学和地理信息领域，GPlates 软件已成为一款颇具影响力的工具，广泛应用于地球物理和地质数据的可视化、板块构造重建、地表动态地形分析等领域。然而，随着 WebGIS 和 WebAssembly 技术的迅速发展，传统的桌面端 GPlates 应用也面临着诸多挑战与改进空间。本章将探讨 GPlates 软件的重构与迁移到 WebAssembly 平台的流程，重点关注其功能模块的拆分、重构以及其在 WebAssembly 环境下的性能提升，为下一章将其成功移植到浏览器和云端的 WebAssembly 平台上，从而实现一种基于 WebGIS 的 GPlates 服务示例应用做准备。GPlates 软件到 WebAssembly 平台的迁移是一项具有挑战性的工作，需要分析和重构整个项目，并且修改数千行代码以完成。

此外，本章节还将探讨 GPlates 软件在迁移过程中可能遇到的问题以及如何解决这些问题。通过这一过程，本论文旨在充分利用 WebAssembly 技术为 GPlates 带来更高效、跨平台的性能表现，同时提高其在地球科学和地理信息领域的应用价值。

3.1 GPlates软件简介

近年来，地球科学研究领域对于板块构造的分析、古地理重建和地球动力学模拟的需求越来越迫切。为满足这一需求，悉尼大学EarthByte工作组、挪威地质调查中心以及加州理工大学的科学家和软件开发者共同创建了一款名为GPlates的开源软件[26]。GPlates能够运行在包括Windows、MacOS以及Linux在内的主流操作系统中，为用户提供交互式板块重建、地理信息系统以及栅格数据可视化等功能的有机组合。用户可以借助 GPlates 对板块重建和相关数据进行直观且灵活的可视化分析操作。

3.1.1 GPlates 软件功能

GPlates 作为一款新世代的板块重建工具，不仅具备传统板块重建软件所具有的功能，例如在用户指定的地质时期和区域进行板块重建和展示、通过鼠标”拖拽”板块到重建位置进行交互式重建、控制重建数据的可视化模式等，还拥有一系列独特的优势。首先，GPlates采用了板块运动模型（plate-motion model），以树状结构的形式描述板块间的相对运动特征；其次，GPlates引入了”连续封闭板块”（Continuously Closed Polygon, CCP）的概念和算法，以解决板块变形区域的重建问题，从而使重建结果更符合地质事实[27]。同时，GPlates 软件还能处理各种几何形态和各种格式的数据，包括栅格数据，使其可视化并进行操作。利用 GPlates 软件平台，用户可以方便地输入数据并生产高质量的图件。

图** 3.1** 桌面端的 GPlates 软件界面截图

为了更全面地利用 GPlates 在地球科学研究中的潜力，研究团队也开发了名为 PyGPlates 的 Python 库[28]，它使得用户能够在 Python 脚本中访问和使用GPlates 的功能，从而实现更加灵活和深入的板块构造分析。PyGPlates库提供了大量的高级和低级功能，使得研究人员可以根据需求进行定制化的操作，例如，pyGPlates.reconstruct() 是一个高级函数，可以将地质数据重建到过去的地质时代。

此外，GPlates 研究团队开发的在线平台 GPlates Web Portal，进一步丰富了 GPlates 的应用场景，为用户提供了 3D 可视化地球物理和地质数据、交互式板块构造重建、交互式地表动态地形以及 PyGPlates 重建服务等功能。GPlates 团队同样基于 PyGPlates 构建了 GPlates Web Service 网络服务，允许用户在不需要本地安装 PyGPlates 的情况下使用其功能。用户可以通过向 https://gws.gplates.org 发送 HTTP请求来获取重建结果，从而在任何编程语言和操作系统上实现板块重建功能。Web服务还实现了容器化，用户可以选择在本地或云端部署 Docker 容器以提高性能和数据安全性[29]。这些在线功能使得GPlates 成为一个更加完善且易于使用的地球科学工具，有助于更高效地推动地球科学研究的发展。

综上所述，GPlates 已成为地球科学研究者在板块构造分析、古地理重建和地球动力学模拟中的重要工具。其开源、免费、易用、功能强大以及专业支持等优势，使得 GPlates 得到了教育工作者、研究人员和行业的广泛使用和认可。事实上，截止到2023年3月10日，已有1487篇与 GPlates相关的论文发表[30]，涵盖地球科学的众多领域。这些论文的数量和质量充分证明了GPlates在地球科学领域的重要地位和实用价值。

3.1.2 GPlates 板块运动模型

GPlates 的核心算法基于板块重建层次结构，该结构是一个描述板块在特定地质时期的总重建极的树形结构。板块运动通过一对板块之间的相对旋转来描述。在模型中，每个板块都相对于另一个板块运动。在这些板块对中，一个板块被视为相对于另一个固定板块的运动板块。而固定板块则相对于另一个板块运动，从而形成了一个树形结构，即重建树。树中的每个相对旋转都是一条边。

以下示意图显示了GPlates中使用的相对旋转层次结构的一个子集：

图** 3.2** GPlates中使用的相对旋转层次结构子集（修改自 GPlates 官方文档[31]）

其中，000 是锚定板块（重建树的顶部）。边 802 相对于 701 包含了 802（板块对中的运动板块）相对于 701（板块对中的固定板块）的旋转。等效旋转是一个板块相对于锚定板块的旋转。因此，板块 802 的等效旋转是从锚定板块 000 到板块 802 的板块回路边路径上的相对旋转的组合。这种板块重建层次结构方法为地球科学家提供了一种有效的手段来解析和理解板块构造的演变过程。

3.1.3 GPlates 现有生态的不足和改进空间

GPlates 作为一款新世代的板块重建工具，在地球科学研究领域具有显著的优势和广泛的应用前景。然而，在当前的技术发展背景下，GPlates 仍存在一些潜在的不足和改进空间，可以引入 WebAssembly 技术，对这些方面进行进一步的探索和改进。

首先，GPlates 门户网站（portal.gplates.org）在渲染方面已经采用了 WebGL 技术，通过 Cesium 库实现了高性能的 3D 地球仪和地图渲染[32]，但依然有较长的渲染与重建时长。因此，GPlates 仍然需要在大规模地理数据处理和可视化的场景中进一步优化渲染效率和板块重建、数据分析性能，以应对不断增长的地球科学数据需求。与此同时，将板块重建放在服务端进行计算，也会消耗大量的服务端计算资源，带来更高的经济开销。为了解决这个问题，GPlates 可以考虑将部分计算任务分发到客户端，通过 WebAssembly（Wasm）技术将 PyGPlates 代码编译为可以在浏览器中运行的高效二进制格式。这将有助于减轻服务器端的计算压力，同时提高客户端的响应速度。例如，可以将一些与地球科学数据交互密切的功能（如数据筛选、简化等）以 C++ 代码的方式编译为 Wasm 字节码放在浏览器中高效执行，从而减少服务器端的负担。

其次，PyGPlates 的 RESTful 服务接口尚不完善，功能覆盖不全。这使得前端在构建 GPlates WebGIS 页面的时候，能完成的功能较为受限，例如无法将重建的数据限制在地球上的特定区域，或进行更加精细化的操作。要实现这一目标，需要修改原先的 GPlates Web Server 并编写更多的 Python 代码，以添加新的后端 API 接口访问低级别的 PyGPlates 功能，才能在前端实现对应的处理逻辑。

此外，GPlates 的云计算支持尚不理想。目前，GPlates 的网络服务主要依赖于容器化技术，而非基于云原生和无服务器构建，导致 GPlates 在云计算环境中的扩展性和弹性受限。未来，GPlates 可以探索采用云原生和无服务器技术，以提高在云计算环境中的可扩展性和弹性。例如，可以将部分功能迁移到无服务器架构，利用按需付费和自动弹性扩展的优势，提高系统的性能和稳定性；对于大规模的板块重建任务，可以将计算任务分割成多个子任务，并将它们分发到多个服务器或云计算节点上。这样，通过并行计算的方式，可以大幅度提高计算效率。同时，考虑采用微服务架构，将不同功能模块分离，以实现更快速的迭代和更新。

尽管 GPlates 在地球科学领域具有显著优势，但在渲染效率、RESTful 服务接口和前端的功能完善程度、云计算支持与可扩展性等方面仍存在较大的改进空间。

3.2GPlates 2.3.0软件结构分析与移植挑战

在本章节中，本论文将探讨将 GPlates 2.3.0 版本[33]从其原生 C++ 桌面应用迁移到基于 WebAssembly（Wasm）的 Web 应用程序的过程。GPlates 2.3.0 是一个功能丰富的地理信息系统，于 2021 年 9 月 8 日发布，是GPlates软件目前可以获取到的最新开源版本，其兼容各种地理数据格式。该版本带来了许多新特性和改进，例如在每个地表点上对岩石圈深度的一维温度平流-扩散方程进行数值求解，提高了地壳稀释计算的稳定性，在大幅度提升了计算性能的同时也修复了一些对应的问题。

为了实现 GPlates 2.3.0 的移植与重构，本论文首先需要获取其开源代码，并对其约 43 万行源代码进行分析。在此过程中，根据 Git记录，本论文需要修改其中大约 7000 行代码。这些修改包括对模块依赖关系的拆分和解耦、依赖库的升级和调整、部分功能和算法的重新实现、以及与 WebAssembly 库或 JavaScripts 库集成的改进。此外，本论文还需要对所有依赖库进行获取、修改和交叉编译，以使其兼容 WebAssembly 环境。在某些情况下，需要在代码中去除对应的依赖库，以简化整个移植过程。

GPlates 2.3.0软件结构分析

本论文对 GPlates 2.3.0 的软件结构进行了深入分析。GPlates 2.3.0 是一个以 C++ 为主要开发语言的开源软件，同时包含一些 Python 脚本。项目使用 CMake 进行配置。为了详细了解 GPlates 2.3.0 的源代码结构，本论文使用 Gocloc 软件对其进行了统计。统计结果显示，GPlates 2.3.0 共包含 2395 个文件，总计 435,091 行有效代码（去除空行和注释），其中 C++ 和 C Header 文件占主要部分，具体如下表所示：

表** 3.1** GPlates 2.3.0 文件与有效代码统计

Language	Files	Blank	Comment	Code
C++	1017	62503	77662	274669
—	—	—	—	—
C Header	1345	49394	115813	153472
XML	3	359	511	2956
CMake	21	141	776	2936
Python	4	103	85	418
XSLT	1	62	26	382
Plain Text	1	26	0	130
XSD	1	17	18	111
C++ Header	1	7	25	12
Bourne Shell	1	2	13	5
TOTAL	2395	112614	194929	435091

从 GPlates 源码中的 DEPS.Linux 文件可知，编译 GPlates 需要安装表 3.2 所示的依赖和库。但对于 Wasm 和 Web 平台，所有的依赖都需要被手动重新构建到 Wasm，或者从源代码中去除。除了下表所示之外，在 Qt 框架中，GPlates 还需要使用以下组件：Core、Gui、Network、OpenGL、Svg、Widgets、Xml 以及 XmlPatterns，这些组件均需要实现 WebAssembly 移植或支持。

表** 3.2** GPlates 2.3.0 依赖库统计

Program/Library	Required Version
cmake	3.5 or newer
—	—
g++	4.8.1 or newer (C++11)
GL library	-
GLU library	-
GLEW library	-
Python library	Version 2 or 3 (preferably 3)
Boost library headers	Version 1.35 or newer (tested up to 1.65)
Qt library	version 5.6 or newer
Geospatial Data Abstraction Library (GDAL)	1.3.2 or newer (GDAL 2 is highly recommended)
Computational Geometry Algorithms Library (CGAL)	4.7 or newer (preferably 4.12 or newer for improved CMake support)
PROJ.4	4.6.0 or newer
Qwt	6.0.1 (6.1.x recommended)
zlib	-

下表是关于 GPlates 中各模块功能的分析和简要概述。每个模块都负责处理和实现 GPlates 软件的不同功能：

表** 3.3** GPlates 2.3.0 模块功能概述

模块	功能描述
data-mining	提供数据挖掘功能，处理和分析地理空间数据
—	—
feature-visitors	实现对地理特征的访问和处理，如数据查询和筛选
file-io	管理文件输入/输出，支持多种地理数据格式
global	包含全局变量和通用函数，供其他模块使用
gui	提供 GPlates 的图形用户界面
maths	包含数学函数和算法，用于进行各种地理空间计算
model	定义数据模型，表示地理特征和属性
opengl	提供 OpenGL 渲染功能，用于在 3D 视图中展示地球和地理特征
presentation	管理数据的可视化和演示，如颜色、线条和符号等
property-values	用于处理地理特征的属性值，如年龄、速度和类型等
qt-resources	包含用于构建 GPlates 的 Qt 资源，如图标和 UI 文件
qt-widgets	提供用于 GPlates 的 Qt 小部件，如工具栏、菜单和对话框等
scribe	用于记录操作和事件，提供撤销/重做功能
unit-test	包含单元测试，用于验证代码的正确性和稳定性
utils	提供实用程序和辅助功能，如字符串处理、时间转换等
view-operations	管理视图操作，如平移、缩放和旋转，以及交互式编辑

在 GPlates 桌面端应用的构建过程中，主要的构建目标包括 GPlates-lib、GPlates、GPlates-no-gui 和 GPlates-unit-test。其中，GPlates-lib 作为核心库，包含了 GPlates 的主要功能模块。GPlates 和 GPlates-no-gui 分别表示具有图形界面和无图形界面的 GPlates 应用程序，它们依赖于 GPlates-lib 以实现其功能。GPlates-unit-test 是针对 GPlates 的单元测试目标，也依赖于 GPlates-lib。具体的依赖关系如下图所示：

图** 3.3** GPlates中的构建目标依赖

3.2.2 移植 GPlates 面对的挑战

在将 GPlates 迁移到基于 WebAssembly 的实现过程中，本论文面临着诸多挑战和困难：首先，GPlates 的模块大部分被编译到 GPlates-lib 中，模块之间存在较强的耦合关系，在进行移植和拆分时，需深入考虑各个模块的功能及其相互关系，去除或重构难以被移植的部分；其次，GPlates 依赖多个外部库，在 2023 年这个时间节点，其中许多库并没有对应版本的 Wasm 支持，或支持相对不完整；此外，本论文需要针对 WebAssembly 环境进行特定的代码优化，以提高加载、执行效率和响应速度。

对于许多应用场景，构建 GPlates-lib 包含了大量不必要的函数和依赖。例如，在仅作为命令行库或板块重建计算库使用时，编译 GPlates-lib 仍需依赖 Qt GUI、OpenGL 等不必要的内容，且包含大量冗余代码，导致二进制体积增大。在 Web 环境中，较大的 Wasm 二进制会显著增加加载时间，影响用户体验。因此，需要尽可能减小二进制代码体积，并在不必要的场景中去除多余依赖。

另一个问题是，在模块化过程中，本论文需确保在 WebAssembly 环境中实现的模块能正常工作，同时尽量减少对其他模块的影响。对于某些模块，如 OpenGL、GLEW和 qt-widgets，由于依赖了大量平台相关的 API，在 WebAssembly 环境中可能需寻找替代方案或进行大量修改，甚至几乎没有办法在有限的时间内完成移植工作，并且进行充分的测试。因此，在不涉及可视化的场景中，例如作为前端板块重建和地理分析计算库，本论文需在移植到 Wasm 平台前尽可能去除其中不必要的部分。

另一个挑战是 GPlates 对多个外部库的依赖。为将 GPlates 移植到 WebAssembly，本论文需要获取、修改并交叉编译所有依赖库至 Wasm，或在代码中修改、去除对应依赖库。这会增加移植的复杂度，可能需投入大量时间和精力完成，例如，GPlates 依赖 Qt5 作为 GUI 库，但是 Qt6 才有对于 Wasm比较良好的支持；在 Wasm 环境中使用的 OpenGL ES 的 API，也和在桌面端运行的 OpenGL 库有较大的区别。

3.3GPlates 到 WebAssembly 的移植与重构

本章将详细介绍将 GPlates 迁移到基于 WebAssembly 的实现过程。在迁移过程中，本论文着重关注 GPlates 的核心功能，如命令行、核心算法库和单元测试等。通过这些移植工作，本论文实现了在 JavaScript 和前端环境中调用 GPlates 的模块，进而可以将 GPlates 集成到其他 Web 应用中；或者在命令行环境中通过云环境下的 Wasm 虚拟机直接执行 Wasm 模块，为后续在云端部署 FaaS 服务提供支持。

值得注意的是，在完成迁移过程后，本论文成功将完整的 GPlates 命令行应用或开发库编译为 Wasm 格式并运行。然而，在可视化方面，由于 OpenGL 和 OpenGL ES（WebGL）在 WebAssembly 环境中存在部分 API 的兼容性问题，GPlates 在 WebAssembly 中的三维可视化功能暂时未能完全通过测试。在后续章节中，本论文将探讨可能的解决方案和替代技术。

在本章中，本论文将逐步介绍 GPlates 到 WebAssembly 迁移过程中的关键步骤和挑战，并针对各个模块的移植工作，讨论遇到的问题和解决方案，以提供一个系统性的迁移指南和参考；同时，也将关注重构和优化的工作，以确保 GPlates 在 WebAssembly 环境中能够正常运行并发挥良好性能。

WebAssembly 环境准备与依赖库构建

为了将 GPlates 迁移到基于 WebAssembly 的实现，本论文首先需要处理应用的外部依赖。GPlates 依赖多个外部库，而这些库需要在 Wasm 环境中可用。在迁移过程中，本论文需要分析这些依赖库在 WebAssembly 上的支持情况，并确定是否需要进行修改、替换或交叉编译。以下将对主要的几个依赖构建进行详细说明：

Qt 与编译工具链支持：

在将 GPlates 迁移到基于 WebAssembly 的实现过程中，本论文面临的首要挑战是处理其对 Qt 库的依赖。GPlates 大量依赖于 Qt 提供的 C++ 基础设施。然而，Qt 5 for WebAssembly仅支持部分 QT 模块，包括 QtBase、QtDeclarative、QtQuickcontrols2、QtWebsockets、QtSvg、QtCharts 和 QtMqtt。这些模块远远不足以满足 GPlates 的需求，因此本论文必须选择升级到 Qt 6 并使 GPlates 兼容此版本。

Qt 6.5 [34]是最新的 Qt for Wasm 支持版本，它为本论文提供了一个稳定的开发平台。Qt 6.5 支持以下组件：Qt Core、Qt GUI、Qt Network、Qt Widgets、Qt QML、Qt Quick、Qt Quick Controls、Qt Quick Layouts、Qt 5 Core Compatibility APIs、Qt Image Formats、Qt OpenGL、Qt SVG 和 Qt WebSockets。这些组件基本上涵盖了 GPlates 所需的 Qt 依赖组件，除了 XmlPatterns。由于 XmlPatterns 的使用较少且不打算投入时间为 Qt 提供适配，本论文决定在 GPlates 源代码中去除或重构所有使用 XmlPatterns 的部分。

为了将 GPlates 移植到 WebAssembly，本论文选择了 Emscripten 3.1.25 作为编译工具链。Emscripten 是一款用于将 C++ 代码编译成 WebAssembly 的工具链，它能够在 Web 端以接近原生速度运行 Qt，无需依赖浏览器插件。根据 Qt for WebAssembly 的官方文档，Emscripten 3.1.25 为本论文提供了所需的支持。本论文在 Windows 11 操作系统上，通过 Qt Creator 10.0.0 和 CMake 工具完成了整个项目的开发和构建。

值得注意的是，当前阶段，Qt for Wasm 的支持仍有待完善，各个模块可能存在许多与其他平台表现不一致的地方。然而，相信随着 Qt for Wasm 的不断更新和升级，这些问题将逐步得到解决。
OpenGL、GLU 和 GLEW 替代方案

在将 GPlates 迁移到基于 WebAssembly 的实现过程中，本论文还需要解决对 OpenGL、GLU 和 GLEW 库的依赖。这些库在原生桌面环境中负责提供 3D 图形渲染能力，在 Web 平台上，本论文需要寻找合适的替代方案，例如 WebGL ，作为底层实现机制。

WebGL 是一种在 Web 平台上实现 3D 图形渲染的技术，它基于 OpenGL ES 规范并与现代浏览器兼容。虽然 WebGL 能够作为 OpenGL、GLU 和 GLEW 库的替代方案，但在迁移过程中，本论文需要面对大量 API 不兼容的问题。为了解决这些问题，本论文对 GPlates 进行了拆分，将与图形界面相关的部分与核心功能分离，这样，核心功能可以在不依赖图形库的情况下正常工作，而图形界面部分可以使用 WebGL 进行重构。本论文可以利用 Qt 和 Emscripten 提供的 OpenGL 到 WebGL 的转换支持，这些工具允许 C++ 代码直接调用 JavaScript API，从而实现与 WebGL 的兼容。为了启用这一功能，需要在编译时使用相应的编译参数，例如 -sFULL_ES3。关于这方面的详细信息，可以参考 Emscripten 的官方文档[39]。尽管本论文已经完成了图形界面部分的重构，但由于 OpenGL Wasm 的实现仍然存在许多与 WebGL 的兼容性问题，因此未能通过测试并正确运行。
Boost 与 CGAL 支持

Boost 和 CGAL 是 GPlates 项目的两个关键依赖库，分别提供了高效、可移植的 C++ 程序库和计算几何算法库。由于它们主要是基于头文件的库（header-only），在将 GPlates 迁移到 WebAssembly 时，可以较为简单地将这些库添加到项目仓库中，并针对 Wasm 目标进行编译。

在迁移过程中，本论文使用了 Boost 1.65 和 CGAL 4.1.4 版本。尽管这些库大部分是 header-only 的形态，但仍然存在一些依赖源文件的 Boost 库，例如 system 库。为了处理这些依赖，本论文需要手动在 CMake 构建脚本中添加对应的编译单元，以确保正确地将这些库构建到 Wasm 目标。

此外，由于 Boost库存在一些与 WebAssembly 不兼容的问题，本论文需要对这些库进行适当的修复，例如修改头文件中的某些工具链内置的 builtin 函数，以适应 WebAssembly 的运行环境和限制。
GDAL 与 PROJ4

GDAL（Geospatial Data Abstraction Library）和 PROJ4 是两个关键的地理空间数据处理库，分别用于翻译和处理栅格和矢量地理空间数据格式，以及进行地图投影转换。

值得注意的是，已经有开源社区对 GDAL 进行了 Emscripten 移植[35]，生成了一个基于 GDAL 2.4 的 WebAssembly 版本。然而，这个移植版本的代码、编译参数和构建脚本存在一些需要进行修复和调整的问题。例如，由于 std::bind2nd 在 Wasm 中不受支持，需要将其替换为 lambda 表达式。PROJ4 是 GDAL 库的依赖，因此在编译时也可以一并被移植，只需最后链接即可。
Python 支持

Python 在 GPlates 中扮演了重要的角色，提供了强大的脚本和扩展功能，然而，在将 GPlates 迁移到 WebAssembly 时，由于 WebAssembly 中的 Python 解释器支持尚不完善，同时受限于 WebAssembly 运行环境不支持进程模型与命令行运行程序，无法启动一个新的进程来运行 Python 脚本。这导致本论文无法直接将现有的 Python 依赖集成到基于 WebAssembly 的 GPlates 版本中。

为了解决这个问题，不得不对 GPlates 进行一定程度的重构，移除所有与 Python 有关的依赖，这意味着在基于 WebAssembly 的 GPlates 版本中，一些依赖于 Python 的功能将不再可用。在未来的场景中，本论文可以探讨其他替代方案，如使用 WebAssembly 兼容的脚本语言（例如 JavaScript）或者利用 Web 技术实现类似的功能，以弥补这一不足。

除了上述讨论的库之外，GPlates 还依赖于其他一些库，如 zlib 等。这些库在编译和迁移到 WebAssembly 平台时，也需要类似的处理和调整。

3.3.2 GPlates 重构与移植

在完成基于 WebAssembly 的环境准备和依赖库构建之后，接下来的关键任务是对 GPlates 源代码进行重构和移植。为了将 GPlates 迁移到 Wasm 并在 Web 页面中使用，本论文需要进行以下几个方面的工作：

移除不可用的依赖库并重构对应的调用部分：对于 GPlates 中不可用或不必要的依赖库，需要移除它们并重构相关的算法和功能实现。例如，所有与 Python 相关的依赖和执行脚本功能、界面、以及相关的数据结构和类都需要被移除。针对 WebAssembly 平台不支持的 Qt XmlPatterns 库的部分内容，本论文使用 Qt XML 库实现相应的算法，主要包括一些 XML 元数据提取功能。此外，还需要重构关于 OpenGL ES 和 GLEW 的部分。

替换或修改不兼容的 API：在源代码中，遇到了一些与 Wasm 不兼容的 API。例如，在 OpenGL ES 中，需要使用 glBufferSubData 替换 glFlushMappedBufferRange 更新缓冲区数据；用 glFramebufferTexture2D 结合不同的纹理目标（例如 gl.TEXTURE_2D，gl.TEXTURE_CUBE_MAP_POSITIVE_X 等）替换 glFramebufferTexture、glFramebufferTexture1D 和 glFramebufferTexture3D，以便将适当类型的纹理附加到帧缓冲区；将 glLoadMatrixd 替换为 gl.uniformMatrix4fv 以在着色器中设置矩阵；以及使用 gl.bufferSubData 替换 glMapBuffer 更新缓冲区数据。

升级 Qt 到 Qt6：由于 Qt5 和 Qt6 之间存在大量不支持的库和 API，如 QGL 和正则表达式相关的内容，需要将 GPlates 项目升级至 Qt6。这将涉及修改和适应新的 API 变化，以确保 GPlates 在 Qt6 环境下能够正常运行。

提高编译选项到 C++17：由于 Wasm 编译工具链的要求，本论文需要将 GPlates 的编译选项提高到 C++17。这涉及对源代码中的某些部分进行调整，以适应新的 C++ 标准，移除一些相对陈旧、Wasm 编译工具链不支持的 C++ 特性，例如 std::auto_ptr、std::random_shuffle() 等。

去除、重构平台相关、不支持的 API：需要移除或重构 GPlates 中与平台相关的、在 Wasm 环境中不支持的 API。这包括进程、线程和命令管理、信号（SIGNAL）等方面的内容，在 GPlates 中，这一部分主要用于执行一些特定的命令或脚本，或者多线程完成后台分析工作。

特殊处理异常：由于 Wasm 目前对抛出异常的支持尚未进入标准，还是草案状态，本论文需要对 GPlates 中的异常处理进行重构，在顶层模块增加一些异常捕获机制，同时在 Emscripten 编译时开启实验性的异常抛出功能，以确保在 Wasm 环境下能够正确地启用异常捕获，或在异常时不至于崩溃退出。

修改文件访问相关部分：Wasm 使用虚拟文件系统，因此本论文需要修改 GPlates 中与文件访问相关的部分，不使用系统的文件访问方式；同时，一些资源文件需要被预先包含进编译好的 Wasm 二进制里进行分发，例如投影的解析数据、GPlates 旋转模型数据等。

模块拆分与优化：本论文将 GPlates 的桌面端应用进行模块拆分和优化，将原先的包含 Qt GUI 部分的 GPlates-lib 拆分成多个库，包括核心的 GPlates-lib（包含板块重建等算法）、GPlates-ui-lib、GPlates-cli-lib 和 GPlates-opengl-lib 等多个构建目标。在这些库之上，本论文构建了 GPlates（完整的 GPlates 应用，包含可视化）、GPlates-cli、GPlates-no-gui 和 GPlates-unit-test 等多个应用，这涉及调整模块之间的头文件的依赖关系，部分模块间的代码修改与迁移，以及启用或停用某些模块中的强耦合功能，并在代码中去除。对于特定的模块，本论文还进行了进一步的拆分和解耦工作，以便于在不同环境中进行灵活配置和使用。新的构建目标依赖关系如下图所示：

图** 3.4** GPlates优化与重构过后的构建目标依赖图

通过以上改进，本论文进一步优化了 GPlates 的源代码结构和功能，使其能够更好地适应基于 WebAssembly 的环境。这将有助于将 GPlates 成功地迁移到 Wasm 平台，并在 Web 页面和云端中运行，为地理信息科学在 Web 平台上的应用提供更多可能性。

3.4 GPlates 功能测试

在完成 GPlates 的重构与移植之后，为确保其在基于 WebAssembly 的环境中正常运行，本论文进行了一系列功能测试。测试的主要目标是验证 GPlates 在 WebAssembly 环境中的核心功能（如板块构造、数据处理、可视化等）是否正常运行，以及性能是否达到预期，为下一步基于 GPlates WebAssembly 开发库，实现 WebGIS 与云端的 GPlates 应用做准备。

测试环境为 Windows 11，Chrome 版本 112.0.5615.138（正式版本）（64 位），搭载 Intel Core i9-12900H 处理器（14 核心）以及 64GB 内存。

为实现这一目标，本论文采取了以下策略：

单元测试：针对 GPlates 中的各个模块和组件，本论文对部分 GPlates 单元测试进行了修复和测试，并通过构建 GPlates-unit-test 应用来执行这些测试。其中部分测试通过，包含 GPlates 的核心算法以及和平台、可视化 GUI 无关的部分，而剩余的部分单元测试由于测试环境、依赖库不支持等各种原因在 WebAssembly 环境下未能通过，且难以进行修复。具体测试列表如下：

表 3.4 GPlates 2.3.0 单元测试在 WebAssembly 中的支持情况

单元测试名称	测试内容	通过情况	可能的原因
ApplicationStateTest	测试应用程序的状态管理和状态变更功能	通过	与WebAssembly兼容
—	—	—	—
CoregTest	测试 Coreg 算法的正确性和性能	通过	与WebAssembly兼容
CptPaletteTest	测试 Cpt 色彩空间的正确性，包括颜色映射和插值方法等	通过	与WebAssembly兼容
DataAssociationDataTableTest	测试数据关联数据表的创建、查询和数据处理功能等	通过	与WebAssembly兼容
FeatureHandleTest	测试 Feature 句柄的创建、查询和操作功能等	通过	与WebAssembly兼容
FilterTest	测试过滤器的创建、应用和性能，包括空间和属性过滤器	通过	与WebAssembly兼容
GenerateVelocityDomainCitcomsTest	测试生成 Citcoms 速度域的算法的正确性和性能	不通过	依赖于特定平台库
MipmapperTest	测试 Mipmapper 的正确性和性能，包括纹理生成和采样方法	不通过	Qt 的 GUI 在 WebAssembly 中支持较差
MultiThreadTest	测试多线程环境下的同步和异步操作的正确性和性能	不通过	WebAssembly对多线程支持有限
RealTest	测试实数数据类型的操作和数学函数的正确性和性能	不通过	WebAssembly虚拟机计算不精确
SmartNodeLinkedListTest	测试智能节点链表的创建、操作和性能，包括插入、删除和遍历等操作	通过	与WebAssembly兼容

JavaScript 功能测试：本论文构建了 GPlates Web 开发库，并在 JavaScript 中调用，完成计算任务。这验证了 GPlates 在 WebAssembly 环境中的可调用性和功能完整性。例如，可以在 JavaScripts 中调用对应的 Wasm API，完成重建工作：

图** 3.5** 在 JavaScripts 中调用对应的 GPlates WebAssembly API 的示意图

简化的 GUI demo：为展示 GPlates 在 WebAssembly 环境下的交互性能，本论文实现了一个简单的包含 Qt GUI 界面的 Web App 示例应用程序。该 demo 包含打开与解析 GPML 配置文件，控制时间节点，调用 GPlates 完成板块旋转与重建，并打印结果等功能，展示了基于 Qt 的 GPlates 应用在 Web 界面上的实际应用能力。

图** 3.6** GPlates WebAssembly Qt GUI 在浏览器中的运行示例应用截图

在演示的这个网页 demo 中，首先创建了三个地理特征（isochrons），即等时线。每个等时线包含以下属性：板块 ID、坐标点、地质时代起始时间、地质时代结束时间、描述、名称以及名称的编码空间。具体来说，分别创建了三个等时线，分别位于印度-非洲板块（Isochron1）、马达加斯加-南极洲板块（Isochron2）和中印度盆地-南极洲板块（Isochron3）。接下来，创建了三个总重建序列（total_recon_seqs），它们表示板块之间的相对运动。每个重建序列包含固定板块 ID、移动板块 ID 以及五元组（时间、纬度、经度、旋转角度、注释）的列表。这些五元组描述了板块在不同地质时代的相对运动。然后，针对不同的时间节点，对这些板块进行了旋转和重建操作。

性能测试：为评估 GPlates-lib 在 Wasm 环境下的性能表现，本论文构建了一组简单的性能测试用例，包括板块重建与旋转、解析 GPML 配置文件与 Features 数据集，坐标转换等，并与在服务器端编译并直接执行 GPlates C++ 代码进行对比。测试结果显示，Wasm 版本的 GPlates 大约比直接执行 C++ 代码慢约 20%，相对存在一些差异，但也远快于使用 JavaScript 重新在前端实现对应功能。相比在服务器端使用原生 C++ 的方式部署 GPlates 应用，也能节省大量的服务器算力资源，此外，采用 WebAssembly 技术也避免了通过网络传输数据给后端进行计算并返回结果的流量消耗与安全问题，对于大多数场景而言，在计算数据量不大时在前端使用 WebAssembly 进行计算都可以获取明显的经济与性能优势。

图** 3.7** GPlates Wasm 和 GPlates 桌面端应用性能对比（WebAssembly 运行环境如上，在 Chrome 中运行。native 为在 x86 架构，Ubuntu 22.04 的Linux 服务器上测试，此处尚未计算数据传输的开销。板块重建与旋转使用上文描述的 demo 中的实现，包含 20 个经纬度的三个地理特征，三个总重建序列，并对于 7 个时间点执行旋转重建操作； GPML 使用了 GPlates 自带的测试 all_caps.gpml 进行解析、处理并输出可读结果；坐标转换采用了前文所述的方式进行测试，使用 5000000 个数据点进行转换）

通过以上测试策略，本论文确保了 GPlates 在基于 WebAssembly 的环境中具有良好的功能表现和性能。这为下一章将 GPlates 在云端和 Web 页面中部署运行奠定了基础，进一步拓展了地理信息科学在 Web 平台上的应用前景。

4基于无服务器计算的GPlates服务实现

随着云原生技术的快速演进，无服务器计算为地理信息科学领域提供了创新性的解决方案。在第三章将 GPlates 核心算法与应用逻辑迁移到 WebAssembly 平台之后，本论文旨在探索将对应的 GPlates 时空数据分析服务部署在 AWS 无服务器计算平台上的可能性，以实现按需计算、高可扩展性和低成本等优势。通过结合 WebAssembly 技术，可以将部分计算任务分配到前端浏览器中，实现高效执行，同时也可以将计算任务部署到云端的无服务器函数计算中进行，从而进一步降低服务端的冷启动开销与计算资源消耗。

为了验证这一概念，本章将基于 GPlates 的 WebAssembly 实现版本，构建一个实证性的应用示例。这一应用旨在展示如何在云端无服务器计算环境中部署与利用 WebAssembly GPlates 进行时空数据分析，以及如何将 WebAssembly 技术应用于前端浏览器中以提高计算效率。本章将系统地阐述基于无服务器计算的 GPlates 服务的设计、实现、部署和优化策略。

4.1设计与实现基于无服务器计算的 GPlates 服务

在本节中，本论文将详细介绍基于无服务器计算的 GPlates 服务的设计思路与实现效果。

需求分析

需求分析是整个系统设计的基础，通过对目标用户群体的需求进行深入了解，可以为后续的系统架构设计和功能设计提供明确的指导。在本节中，将分析 WebAssembly GPlates 应用在云端和 Web 端部署的需求，包括功能需求和技术需求等方面。本论文力求将 WebAssembly 技术的优势与 GPlates 服务相结合，以实现高性能、高可扩展性、低成本和易用性的时空数据分析服务。

功能需求：

数据分析功能：用户关心的核心功能之一是能够在云端或网页端进行快速、准确的时空数据分析。这包括板块构造重建、坐标转换、空间分析、数据挖掘等各种数据处理功能，具体而言，GPlates 应用应支持板块运动的可视化、板块边界的识别、地质年代数据的配置和解析等任务。
用户交互：用户希望能够通过一个友好、直观的界面来操作 GPlates。这包括地图浏览、数据输入、参数设置以及分析结果展示等。为了提高用户体验，GPlates 应用应当支持多种地图视图切换、拖拽和缩放地图、地图元素的点击、重建年代的配置等交互功能。
数据管理：用户需要能够轻松地上传、下载、编辑和管理他们的数据集。此外，还需支持多种数据格式，如 Shapefile、GeoJSON、CSV 等。为满足这一需求，GPlates 应当提供数据导入导出模块和数据验证功能，同时还可以实现数据的云端存储和实时同步。

技术需求：

可扩展性：随着用户数量和数据量的增长，系统应能够自动扩展以满足不断增长的需求，确保服务的稳定性和可用性。本论文可以将 GPlates 时空数据分析服务部署在无服务器计算平台上，实现按需计算、高可扩展性和低成本的优势。
性能：在云原生时空数据分析场景下，分析任务的处理速度和可视化响应时间至关重要。因此，系统需要具备高性能的计算能力，以便快速完成各种时空数据分析任务，力求获得不逊色于桌面端应用的数据分析与计算能力。同时，通过优化前端体积可以实现快速加载和执行，从而提高用户体验。
安全性：数据的安全和隐私是用户非常关心的问题。因此，系统需要采取严格的安全措施，如加密传输、访问控制和数据备份等，以确保用户数据的安全性。
兼容性：系统需要支持各种主流浏览器和设备，以便用户在不同环境下使用。此外，还需考虑如何在现有的云服务平台上进行快速部署和集成，以便快速搭建云原生时空数据分析服务。
经济性：对于 GPlates 一类访问量较小的 WebGIS 应用，或峰谷流量差异较大的应用而言，需要尽可能节约部署上线的成本，降低资源消耗。

对以上需求的深入分析可为基于无服务器计算的 GPlates 服务的系统架构设计和功能设计，提供明确的指导思路。

系统架构设计

为了实现基于无服务器计算的 GPlates 服务，本论文提出了一种具有高性能、可扩展性和易用性、经济的系统架构。图 4.1 展示了整个系统的架构，包括前端应用、API 网关、Lambda 函数、数据存储和用户认证等组件。整个系统架构分为四层，分别是前端组件部分、网关与接入层，业务逻辑与时空数据分析逻辑，数据存储和其他服务。在图中，前端界面通过 API 网关与多个 Lambda 函数进行通信，而 Lambda 函数则与数据存储和用户认证服务进行交互。各个组件之间的连接以及数据流向可以通过图表更加直观地展示。

图** 4.1** GPlates Serverless Web 应用的架构设计图

在以下各小节中，本论文将详细阐述这些组件的设计和功能，以及它们之间的相互关系和数据流向。

前端应用 ：前端应用采用 Web 技术和 WebAssembly 构建，提供用户友好的交互界面，用于展示地图、数据输入、参数设置、计算和分析结果等。为了降低系统延迟，部分计算任务可以在前端执行，而不是发送到后端的无服务器函数进行处理，用户可以根据数据集大小和后端服务器是否支持，自由选择是否将数据发送到对应的无服务器函数式计算中进行处理。前端应用可以通过 API 网关与后端服务进行通信，将用户的请求发送给相应的 Lambda 函数，同时负责显示来自 Lambda 函数的分析结果和其他数据。

API 网关与 Lambda 函数：API 网关（如 AWS API Gateway）负责路由和管理来自前端的请求，将请求分发给相应的 Lambda 函数。API 网关还可以实现安全性、流量控制和监控等功能，保障系统的稳定运行。Lambda 函数基于无服务器计算框架编写，可以用于处理各种时空数据分析任务或后端应用逻辑。每个 Lambda 函数负责一个特定的功能，如板块构造分析、地理坐标转换等。Lambda 函数能够根据实际需求自动扩展，提供弹性计算能力。此外，将不同功能封装在独立的 Lambda 函数中有助于实现模块化设计，便于代码维护和迭代。

图** 4.2** AWS Lambda 和 API 网关的调用流程示意图[36]

通过将 WebAssembly 模块部署到 AWS Lambda 无服务器计算平台，本论文实现了高性能、安全性、跨平台兼容性以及易于维护与管理的时空数据分析应用。具体实现的方式是借助 WasmEdge Serverless Runtime 和 AWS Lambda 运行时接口客户端（RIC）的集成，在 Lambda 上运行了基于 WebAssembly 的 GPlates 应用。这种部署方法为云原生时空数据分析带来了显著的优势，且有助于降低延迟、提高整体性能和安全性，同时简化了应用程序的部署和管理过程。

图** 4.3**将WebAssembly 函数部署到AWS Lambda 中[37]

数据存储与用户认证 ：数据存储组件包括云存储服务和无服务器数据库服务。云存储服务（如 AWS S3）负责存储用户上传的数据文件，确保数据的安全性和可扩展性。元数据则存储在无服务器数据库服务（如 Amazon DynamoDB 或 Amazon Aurora Serverless）中，根据实际需求自动调整容量，以满足大规模应用的数据存储需求。

图** 4.4** Amazon DynamoDB特性与应用场景[38]

用户认证集成了云平台提供的认证服务（如 AWS Cognito）实现用户登录验证。用户认证服务将负责管理用户的注册、登录和权限控制等功能。通过集成云平台提供的认证服务，可以简化用户认证流程，提高系统的安全性和可用性。

图** 4.5** Amazon Cognito[39]

第三方 GIS 服务：为了支持更丰富的地理信息功能，本系统还整合了第三方 GIS 服务，如 Amazon Location Service 等。这些服务为系统提供额外的地理信息数据、地理坐标转换、地图样式等功能，从而使得 GPlates 服务能够提供更加完整和丰富的时空数据分析功能。

通过上述各组件的设计，本系统实现了一个基于无服务器计算的 GPlates 服务，充分利用了云计算资源，具有高性能、可扩展性和易用性等特点。在后续章节中，本论文将详细讨论各个功能模块的设计和实现。

前端界面布局设计与实现

在本节中，将详细介绍基于无服务器计算的 GPlates 服务的前端设计与实现。本论文设计了一个清晰、简洁的界面布局，使用户能够轻松地找到所需的功能和设置。

前端技术栈选择：本论文使用 AWS Amplify [40]和 React 构建前端应用。AWS Amplify 是一个集成的开发平台，提供了简化的开发和部署流程，可以快速搭建和管理前端应用。React 是一个轻量级且功能强大的前端框架，易于学习和使用。为了进一步优化前端性能，本论文采用了 WebAssembly 技术将一些计算密集型任务在前端完成，从而减轻服务器端的负担。此外，本论文使用 D3.js 完成地图可视化部分，实现地图展示与交互。

本论文设计了一个清晰、简洁的界面布局，分为地图可视化区域、数据集输入和管理区域、参数设置区域，以及计算区域等。地图区域用于展示地理数据，如底图、板块边界、热点等；数据输入区域用于用户上传数据文件；参数设置区域允许用户实时调整参数并观察其对计算结果的影响；计算结果展示区域展示板块构造分析等计算结果。前端应用包含以下主要组件：

FeatureCollections：负责处理地理数据集的输入、管理和展示。
GPlatesCodeEditor：提供板块构造分析的代码编辑器、执行结果输出和聊天窗口。
GPlatesD3Visualization：实现地图可视化与交互，包括地图展示、控制面板、数据输出和侧边栏。
Tabs：负责界面导航和组件切换。

下图展示了前端界面的布局和各个组件之间的关系：

图** 4.6** GPlates Web 前端界面布局效果截图

图** 4.7** GPlates Web 前端的架构设计与组件依赖图

数据输入与参数设置：本论文设计了一个易用的数据输入与 Features 管理界面，使用户能够轻松地上传数据文件和输入相关参数。数据输入区域支持文件选择上传，并提供数据格式校验和错误提示功能，确保用户输入的数据符合要求。此外，本论文还使用前端技术实现动态参数设置，使用户能够实时调整参数并观察其对计算结果的影响。

地图展示与交互：使用 D3.js 实现地图数据的展示，包括底图、板块边界、热点等。本论文实现了地图的基本交互功能，如缩放、平移、点击查看详情等。为了提高用户体验，本论文采用了 WebAssembly 技术优化地图渲染性能，确保用户可以流畅地操作地图。

用户认证与前后端通信：本论文使用 AWS SDK 完成用户认证，提供登录验证、注册等功能。前端应用通过 API 网关与后端 Lambda 函数进行通信，将用户的请求发送给相应的处理函数。同时，本论文使用了云服务 SDK（如 AWS SDK）简化前端与后端之间的通信，提高数据交互的效率。为了保证前端界面在等待后端处理结果时保持响应，本论文实现了请求的异步处理。

综上所述，本论文基于 AWS Amplify、Vue.js 和 D3.js 等技术栈实现了一个清晰、简洁且功能丰富的前端界面，使用户能够轻松地进行时空数据分析。通过采用 WebAssembly 技术、实现异步通信和性能分析优化等方式，本论文确保了前端应用的高效运行。在后续章节中，本论文将深入讨论后端处理、数据存储和分析等方面的实现细节。具体的界面效果，也可在后文查看。

前端可视化设计与实现

在本节中，将详细介绍基于无服务器计算的 GPlates 服务的前端可视化设计与实现。为了提供丰富的可视化体验，本论文实现了以下功能：支持上传、选择和展示 features；实现二维和三维地球显示；支持拖拽移动、放大、缩小；以及显示点、多边形等 features。以下流程图展示了前端可视化工作流程的各个步骤，以及它们之间的相互关系：

图** 4.8** GPlates Web可视化板块重建流程图

上传和选择 features：本论文设计了一个简单易用的界面，允许用户上传和选择 features。用户可以通过点击按钮或拖放文件的方式上传地理信息数据文件，如 GeoJSON 或 GPlates 文件。文件上传后，本论文将文件解析成 features，并将其显示在可视化界面上供用户选择。

图** 4.9** GPlates Web上传和选择 features效果截图

二维和三维地球显示：前端可视化部分支持以二维和三维地球方式显示。用户可以根据需要切换显示模式。在二维模式下，地图以平面投影的方式呈现；在三维模式下，地图以球体的方式呈现。本论文使用 D3.js 和 WebGL 技术实现这两种显示模式。

图 4.10** GPlates Web**以三维球体的方式显示可视化界面和点Feature效果截图

拖拽移动、放大、缩小：为了增强用户体验，本论文实现了拖拽移动、放大、缩小等交互功能。用户可以通过鼠标或触控设备对地图进行拖拽移动、放大和缩小，以便更好地查看地理信息。

图** 4.11** GPlates Web 放大并显示多边形 Feature 的效果截图

显示点、多边形等 features：本论文实现了支持显示点、多边形等 features 的功能。用户上传的地理信息数据文件解析后，本论文将 features 渲染到地图上。使用 D3.js 和 WebGL 技术，本论文可以高效地在地图上绘制各种类型的 features。

根据滚动条选择年代进行旋转和重建：本论文实现了一个滚动条，允许用户选择不同的年代。通过滚动条选择年代后，前端应用将执行板块重建和旋转等计算，根据计算结果更新地图显示。这一功能使用户能够直观地观察地球在不同年代的形态变化。

图** 4.12** GPlates Web使用滚动条选择年代为 70 Ma 的效果截图

综上所述，本论文实现了一个功能丰富的前端可视化界面，为用户提供了便捷、直观的时空数据分析体验。在后续章节中，本论文将进一步讨论后端处理、数据存储和分析等方面的实现细节。

1.

API 网关与函数即服务设计与实现

在本节中，将详细介绍基于 AWS 的 API 网关与AWS Lambda 函数的 GPlates 后端逻辑设计与实现，以便为前端提供一个可靠、易用且高性能的 GPlates RESTful API。本论文配置了 API Gateway 作为 AWS Lambda 函数的触发器，每当收到 API 请求时，API Gateway 将触发对应的 Lambda 函数，如下所示：

图** 4.13** GPlates 板块重建 API触发配置截图

本论文使用 AWS API Gateway 创建和管理 API，并将其与 AWS Lambda 函数进行集成。API Gateway 提供了一个全托管的服务，能够处理所有 API 请求的授权、访问控制和跨域问题。本论文配置 API Gateway 以便正确转发请求到相应的 Lambda 函数。在此之上，本论文设计了一个合理的 API 路由结构，以便将不同请求分发到对应的 Lambda 函数进行处理。本论文保持了与 GWS（GPlates Web Service）类似的 API 结构，采用了类似于 GWS 的 API 部署，例如：GET /reconstruct/reconstruct_points/、GET /earth/get_globe_mesh/、GET /info/model_names/ 等。这些 API 提供了丰富的功能，包括地球物理特征重建、地球模型查询和模型元数据查询，具体的 API 列表如下：

图** 4.14** GPlates RESTful API 配置截图

API 安全与认证：本论文使用 AWS Cognito 和 API Gateway 为API 提供安全的用户认证和授权。通过使用 JSON Web Tokens（JWTs）进行身份验证，本论文确保了只有经过验证的用户才能访问 API。

GPlates 功能的封装与部署：本论文将 GPlates 的功能封装为独立的 WebAssmebly 模块，这些模块可以被 AWS Lambda 函数导入和使用。本论文遵循了 AWS Lambda 函数的编写规范，并将函数打包为一个部署包，包含所需的依赖和二进制文件。这些 AWS Lambda 函数负责处理来自 API Gateway 的请求，并将结果返回给前端。

为了将 WebAssembly GPlates 模块部署到 AWS Lambda 的过程中，需要选用 AWS Lambda 的 Node.js Docker 镜像作为构建基础，该映像内置了 Lambda 运行时接口客户端（RIC），满足了 AWS Lambda 的操作需求。其次，本论文需要将函数及其相应的依赖项放置在 /var/task 目录下，以便 AWS Lambda 能够正确地执行这些文件。接着，设定容器启动时的默认命令，确保在每次调用无服务器函数时，都能触发相应 JavaScript 文件中的处理程序函数，然后调用对应的 Wasm 模块完成真正的计算任务。通过这一系列步骤，基于 WebAssembly 的 GPlates 模块成功地部署到了 AWS Lambda 上，为时空数据分析提供了云端支持。

以下是部署的 AWS Lambda 函数列表，本论文通过在 API 网关上挂载这些函数，使得它们在请求到来时被自动执行：

图** 4.15** GPlates AWS Lambda部署配置截图

函数监控与日志管理：为了监控 Lambda 函数的执行情况和性能指标，本论文使用了 AWS CloudWatch [41]，并配置了 CloudWatch日志组，以便将 Lambda 函数的日志输出保存到 CloudWatch Logs。这使本论文能够实时检查函数的运行情况、错误信息和性能指标，以便及时调整资源分配和优化代码。

图** 4.16** GPlates Web Service Amazon CloudWatch监控图表截图

综上所述，在本节中详细介绍了 AWS Lambda 函数与 API 网关部分的设计与实现，实现了无服务器计算架构下 GPlates 服务的后端处理。

数据存储与访问设计实现

在本节中，将详细介绍数据存储与访问的设计实现，以支持基于 WebAssembly 的云原生时空数据分析技术在 GPlates 服务中的应用，并将重点讨论数据存储方案、数据访问和处理的优化，以及数据安全性和一致性保障。

数据存储方案：Amazon S3 [42]提供了高可用性、高持久性和低延迟的对象存储，非常适合存储大量的地理数据和模型文件。为了实现高性能、可扩展且低成本的数据存储，本论文采用了 Amazon S3 作为 GPlates 数据的主要存储服务，并根据需求分配了对应的 S3 存储桶，用于存放用户上传的数据文件：

图** 4.17** GPlates Web Service Amazon S3 文件存储桶配置截图

在 AWS Amplify 后台，可以查看对应用户上传的数据集文件：

图** 4.18** GPlates Web Service Amazon S3 后台文件管理截图

数据访问与处理优化：本论文使用 Amazon DynamoDB 作为元数据和请求状态信息的存储服务，以实现低延迟的数据访问。DynamoDB 是一个完全托管的 NoSQL 数据库服务，具有高性能、高可扩展性和低成本的特点。同时，本论文使用 AWS Identity and Access Management (IAM) 对数据访问进行严格的权限控制，确保只有授权的用户和服务能够访问数据；也启用了 Amazon S3 的版本控制功能，以便在数据发生变更时保留历史版本。

用户认证与授权设计实现

在本节中，将详细介绍用户认证与授权的设计实现，以确保基于 WebAssembly 的云原生时空数据分析技术在 GPlates 服务中的安全使用，并将重点讨论认证服务选型、权限管理策略。

用户认证：为了实现简单、安全且可扩展的用户认证，本论文选择了 AWS Cognito 作为 GPlates 服务的认证服务。AWS Cognito 提供了用户池和身份池两种认证方式，支持社交身份提供商、企业身份提供商以及自定义认证服务。本论文根据 GPlates 服务的需求，配置了用户池并启用了多种认证方式，以便用户可以使用电子邮件进行注册和登录，同时还利用 Cognito 的预设触发器实现了自定义认证逻辑，以满足特定场景的安全要求。

图 4.19 GPlates 用户组截图

本论文通过以下流程图展示了 GPlates 服务的用户认证流程，包括注册和登录两个部分。在注册过程中，用户需要输入邮箱和密码，获取并输入验证码，最后完成注册。在登录过程中，用户输入邮箱和密码，系统判断登录是否成功，成功则进入系统，否则显示错误信息。

图** 4.20** GPlates 用户认证流程截图

为了提供直观的用户体验，本论文设计了简洁且易于操作的登录与注册页面。用户可以轻松完成注册与登录操作，从而进入 GPlates Web 应用系统。

图** 4.21** GPlates Web 应用用户登录界面截图

图** 4.22** GPlates Web应用用户注册界面截图

本论文设计了合理的用户权限管理策略，确保用户只能访问自己有权访问的资源。本论文使用 AWS Identity and Access Management (IAM) 对 GPlates 服务中的资源进行分级管理，并为不同类型的用户分配了相应的权限角色。具体地，本论文将用户分为管理员、普通用户和访客等角色，根据角色的不同为其分配不同的访问权限。此外，本论文还利用 AWS Lambda 函数实现了细粒度的访问控制，以保障数据和功能的安全使用。

图** 4.23** GPlates Web 应用用户管理后台截图

综上所述，本节详细介绍了用户认证与授权的设计实现，以确保基于 WebAssembly 的云原生时空数据分析技术在 GPlates 服务中的安全使用。

4.2部署与优化

在本节中，将详细介绍基于 WebAssembly 的云原生时空数据分析技术在 GPlates 服务中的部署与优化策略，重点讨论应用的持续集成与持续部署（CI/CD）流程、性能优化、以及成本控制策略等方面。

持续集成与持续部署（CI/CD）：为了实现高效且可靠的应用部署，本论文采用了 AWS CodePipeline[43]构建了完整的 CI/CD 流程。本论文利用 Github 作为代码仓库，当有 Commit 推送到 Github 仓库时， AWS CodeBuild 会自动进行应用的构建与测试，最后使用 AWS CodeDeploy 实现自动部署到生产环境，在 AWS 上的构建与部署示意图如下图所示：

图 4.24 GPlates Web 部署流水线截图

在整个过程中，本论文遵循了 DevOps 的最佳实践，包括基于分支的开发策略、自动化测试、以及基于环境的部署策略。此外，本论文还利用 AWS CloudFormation 实现了基础设施即代码（IaC），以确保资源的一致性与可复用性。

性能优化：为了提高基于 WebAssembly 的云原生时空数据分析技术在 GPlates 服务中的性能，本论文采用了多种优化策略。首先，在 Lambda 函数层面，本论文针对不同的计算任务为函数分配合适的内存和执行时间；其次，在数据存储与访问层面，本论文利用 Amazon S3、DynamoDB 和 CloudFront 实现了高性能的数据存储、访问与分发。此外，本论文还对前端应用进行了优化，包括减少静态资源的体积、使用浏览器缓存策略以及采用懒加载等技术。打包并压缩后的 Wasm 应用体积仅约为 8 MB，在大部分的网络环境下可以在数秒到数十秒内完成下载、加载流程。

成本控制策略：为了在保证应用性能的同时控制成本，本论文采用了多种成本控制策略。首先，在计算资源方面，本论文充分利用了 AWS Lambda 的按需付费模式，根据实际使用情况分配资源，以减少不必要的支出。其次，在数据存储方面，本论文使用 Amazon S3 提供的存储类型（例如 One Zone-IA 和 Glacier）来降低长期数据存储成本。此外，本论文还利用 AWS Budgets 和 AWS Cost Explorer 对整个项目的成本进行监控与预测，以确保成本在预期范围内，如图所示：

图 4.25 AWS Cost Explorer 监控图表截图

4.3性能与资源消耗评估

性能指标：为了全面评估 GPlates 服务的性能，本论文采用了多种性能指标。首先，本论文关注应用响应时间，即从用户发起请求到接收到响应所需的时间，并对 GPlates 服务进行了对应的功能测试，发现平均响应时间为 150ms，95% 响应时间低于 400ms。此结果表明，GPlates 服务在正常负载下具有良好的响应时间。

此外，本论文还关注吞吐量，即单位时间内处理的请求数量。吞吐量指的是单位时间内处理的请求数量，直接影响到系统能够承受的并发用户数量。为了评估 GPlates 服务在高负载情况下的性能表现，本论文进行了负载测试，模拟了 1000 个并发用户访问服务的场景。实验结果显示，在不进行预先配置的情况下进行并发请求和扩容，在初始阶段的以约每分钟增加 500 个实例的速度扩容结束后，系统在 1 分钟内可处理约 1000 个请求，最高并发数可达上百个用户。此外，在高并发访问情况下，GPlates 服务能够保持稳定性能，显示出良好的可扩展性。这一简要的测试结果受限于 AWS 的可扩展性配置，与预置的 Lambda 函数实例数量[44]。

Amazon CloudWatch 监控服务收集和分析资源消耗数据，旨在了解系统的运行状况及优化需求。研究结果显示 Lambda 函数性能与资源分配均具有合理性，在本论文的测试期间，平均执行时间约为 300ms，平均内存使用为 200 MB，错误率低于 0.01%。鉴于 GPlates 作为一种学术性质的 WebGIS 服务，其在论文发布前后的访问量峰值远大于日常访问请求。AWS Lambda 免费套餐提供每月 100 万次免费请求和 400,000 GB-秒的计算时间，支持 x86 和 Graviton2 处理器或两者结合的函数。假设每日约有 100 名用户使用 GPlates 的可视化服务，每次使用产生约 300 次板块重建请求，每月的消耗仍在 AWS Lambda 的免费套餐范围内。

相较于使用云端虚拟机部署，基于 AWS Lambda 的部署方式具有显著优势。我们同样尝试在 AWS 上部署了原生的 GWS（GPlates Web Service）的容器实例，在功能上相同的情况下，该容器镜像体积约为 2.92 GB，以执行4个点的简单旋转任务为例（points=95,54,142,-33&time=140&model=SETON2012），内存占用为 386.3MB 。以 AWS EC2 实例为例，满足运行基于容器的 GPlates 服务需求的最少实例为 1 核 0.5G 内存，20GB SSD 硬盘，每月仍需 22.5 元的费用。因此，根据上述估计，对于访问量不高、峰谷差异明显的 GPlates 应用来说，它的 WebAssembly 模块在 AWS Lambda 上的部署成本更为经济。此外，AWS Lambda 具有自动扩展功能，可根据实际需求动态调整计算资源，从而提高资源利用率，降低总体硬件成本和人力运维成本。

5 结论与展望

5.1研究存在的问题与展望

尽管本论文在云原生时空数据分析技术的发展探索方面取得了一定成果，但仍存在一些不足之处，需要在未来进一步完善：

首先，在 GPlates 软件迁移过程中，部分功能模块因 WebAssembly 技术限制和库的支持未能完全实现，没有办法将 GPlates 桌面端的功能完全在浏览器中运行，但随着工具链和库的完善，这一部分在未来实现的难度将大大降低。例如，由于 OpenGL ES 的支持不完全，以及 Qt for Wasm 中的 xmlpattern 库不被支持等问题，部分 GPlates 可视化功能没有完全移植成功。未来研究需在 WebAssembly 技术发展的基础上，逐步完善这些功能模块的迁移与重构，尤其是改进和完善 GPlates 可视化部分，并积极向开源软件上游贡献对应的代码。同时，应进行更为完善的测试和性能分析，尤其是针对 GPlates 的常用工作负载进行实际验证，以确保软件功能的稳定性和可靠性。

其次，针对大规模地球科学数据的处理与分析，由于目前并未针对 WebAssembly 的使用场景和技术进行进一步的优化，仍存在一定的性能瓶颈。为改善性能表现，未来研究应更加关注优化算法、提高计算资源利用率等措施，以便充分发挥云计算平台和浏览器中 WebAssembly 运行时的潜力。此外，本论文中所实现的云原生无服务器 GIS 应用仅在 AWS 云平台上进行了部署和简单的功能测试和性能测试，具有一定局限性，未来研究应将其扩展到其他云计算平台，同时实现更完整的数据分析和板块重建功能，以适应多样化的地球科学研究需求。

5.2研究结论

本论文针对云原生时空数据分析领域和 WebGIS 领域的技术挑战，提出了一种基于 WebAssembly 的解决策略，并以 GPlates 软件为实证研究对象。通过深入探讨基于 WebAssembly 的 Web 时空数据分析与可视化技术，本论文实现了GPlates 软件的重构与迁移到 WebAssembly 平台，并在浏览器或云端中运行了对应的功能。研究成果表明：通过 GPlates 软件板块构造重建和 GIS 空间分析等关键功能模块的细致拆分与重构，并将 GPlates 功能模块移植到 WebAssembly 平台，本论文为 WebGIS 应用提供了更完备的 GPlates 功能，同时不仅有效提升了 GPlates Web 应用的计算性能和渲染效率，还减少数据了在网络传输过程中的泄露风险，更好地保护用户的隐私数据与安全性，拓展了其在地球科学研究领域的应用场景。

在将 GPlates 功能模块移植到 WebAssembly 后，本论文详细讨论了基于 WebAssembly 的云原生时空数据分析技术，在 GPlates Web 服务中的实现、部署与优化策略，并系统地分析了基于 WebAssembly 的云原生计算模型及其优势，阐述了 WebAssembly 技术在提升计算性能和渲染效率方面的潜力，并详细设计实现了 GPlates 服务中的各个模块，包括 AWS Lambda 函数、API 网关、数据存储与访问、以及用户认证与授权等方面。在部署与优化方面，本论文采用了持续集成与持续交付（CI/CD）、性能优化和成本控制策略，确保 GPlates 服务的高效运行。

最后，本论文评估了基于 WebAssembly 的 GPlates 无服务器 WebGIS 应用的性能和资源消耗，和传统的基于容器部署 Web 服务的方式对比，在功能上相同的情况下，这种部署方式不仅显著提高了系统的运维效率，大幅度降低了开发部署成本，还能在面临负载变化的情况下实现自动扩缩容等功能。本论文为云原生时空数据分析技术的发展探索了新的理论和实践基础，对相关领域具有一定的参考意义。

参考文献

Amazon Web Services. Amazon Elastic Compute Cloud (Amazon EC2) [EB/OL]. 2006. [2023-05-23] https://aws.amazon.com/cn/ec2/.
Bhat M A, Shah R M, Ahmad B. Cloud Computing: A solution to Geographical Information SystemsGIS. International Journal on Computer Science and Engineering, 2011, 3(2): 594-600.
Alfaqih T M, Hassan M M. GIS Cloud: Integration between cloud things and geographic information systems (GIS) opportunities and challenges[J]. International Journal on Computer Science and Engineering, 2016, 3(5): 360-365.
Amazon Web Services. Amazon Lambda [EB/OL]. [2023-05-23] https://aws.amazon.com/cn/lambda/.
Shillaker, Simon, and Peter Pietzuch. “Faasm: Lightweight isolation for efficient stateful serverless computing.” arXiv preprint arXiv:2002.09344 (2020).
Long J, et al. A lightweight design for serverless function as a service[J]. IEEE Software, 2020, 38(1): 75-80.
Ranum A, Liu J, Carter D. What’s Up With WebAssembly: Compute’s Next Paradigm Shift [EB/OL]. [2023-05-23] https://sapphireventures.com/blog/whats-up-with-webassembly-computes-next-paradigm-shift/.
Björk F. Announcing Grafbase: Instant serverless GraphQL backends [EB/OL]. [2023-05-23] https://grafbase.com/blog/announcing-grafbase.
Esri. ArcGIS Online Overview [EB/OL]. [2023-05-23] https://www.esri.com/en-us/arcgis/products/arcgis-online/overview.
Agrawal S, Gupta R D. Web GIS and its architecture: a review[J]. Arabian Journal of Geosciences, 2017, 10(1): 1-13.
Müller D, Qin X, Sandwell D. The GPlates Portal: Cloud-based interactive 3D and 4D visualization of global geological and geophysical data and models in a browser[C]. EGU General Assembly, Vienna, Austria, April 23-28, 2017.
WebAssembly. WebAssembly [EB/OL]. [2023-05-23]. https://webassembly.org/.
Wikipedia contributors. WebAssembly[J]. In Wikipedia, The Free Encyclopedia, 2023, May 5. Retrieved 10:12, May 8, 2023, from https://en.wikipedia.org/wiki/WebAssembly.
WebAssembly. Roadmap[EB/OL]. 2017. [2023-05-23] https://webassembly.org/roadmap/
Kolak M, et al. The US COVID Atlas: A dynamic cyberinfrastructure surveillance system for interactive exploration of the pandemic[J]. Transactions in GIS, 2021, 25(3): 634-649.
Cesium. CesiumJS[EB/OL]. (n.d.). Cesium. https://cesium.com/platform/cesiumjs/.
SuperMap. SuperMap iEarth [EB/OL]. (n.d.). [2023-05-23]．https://supermap.github.io/SuperMap-iEarth/.
CNCF. CNCF Wasm Microsurvey: A Transformative Technology – Yes, But Time to Get Serious[EB/OL]. 2022, October 24. https://www.cncf.io/blog/2022/10/24/cncf-Wasm-microsurvey-a-transformative-technology-yes-but-time-to-get-serious/.
Scheuner J, Leitner P. Function-as-a-service performance evaluation: A multivocal literature review[J]. Journal of Systems and Software, 2020, 170: 110708.
WebAssembly. WebAssembly/design [EB/OL]. (n.d.). [2023-05-23]．https://github.com/WebAssembly/design.
Unity Technologies. WebAssembly is here![EB/OL]. 2018, May 30. [2023-05-23] https://blog.unity.com/technology/webassembly-is-here.
Decovar. Qt WebAssembly Custom OpenGL[EB/OL]. 2021, August 29. [2023-05-23] https://decovar.dev/blog/2021/08/29/qt-webassembly-custom-opengl/.
Shcherbinin K. QGIS and WebAssembly[EB/OL]. 2022. [2023-05-23] https://wonder-sk.github.io/Wasm/qgis.html.
Emscripten. OpenGL support [EB/OL]. n.d. [2023-05-23]. https://emscripten.org/docs/porting/multimedia\_and\_graphics/OpenGL-support.html.
Emscripten. Emscripten [EB/OL]. 2023 [2023-05-23]. https://emscripten.org/.
Müller R D, et al. GPlates: Building a virtual Earth through deep time[J]. Geochemistry, Geophysics, Geosystems, 2018, 19(1). 2018. https://doi.org/10.1029/2018GC007584.
Mather B R, et al. Deep time spatio-temporal data analysis using pyGPlates with PlateTectonicTools and GPlately[J]. Geoscience Data Journal, n.d., n.p. n.p.: n.p., n.d. https://doi.org/10.1002/gdj3.185.
Williams, S., Cannon, J., Qin, X., … & Müller, D. (2017). PyGPlates-a GPlates Python library for data analysis through space and deep geological time. EGU General Assembly. https://ui.adsabs.harvard.edu/abs/2017EGUGA..19.2828W
Yang, X., & Smith, G. C. (2023). A review of the Gippsland Basin history based on comparison of 3D structural, stratigraphic and forward sedimentation models: recognition of source, reservoir, traps and canyons[J]. Australian Journal of Earth Sciences, 2023, 70(2): 149-174. 2023.
GPlates. Publications [EB/OL]. n.d. [2023-05-23]. https://www.GPlates.org/publications/
GPlates. PyGPlates foundations [EB/OL]. n.d. [2023-05-23]. https://www.gplates.org/docs/pygplates/pygplates\_foundations.html.
Gurnis, M., Müller, D., Cannon, J., … & Talsma, A. (2018). GPlates and pyGPlates: Open-source software for building a virtual Earth through deep time. AGU Fall Meeting. https://ui.adsabs.harvard.edu/abs/2018AGUFM.T11B2671G
GPlates. GPlates 2.3 released [EB/OL], 2021 [2023-05-23]. https://www.GPlates.org/news/2021-09-08-GPlates-2-3-released/
Qt. WebAssembly [EB/OL]. n.d. [2023-05-23]. https://doc.qt.io/qt-6/Wasm.html
Dohler, D. GDAL-JS [EB/OL]. Place unknown: GitHub. (n.d.) [2023-05-23]. https://github.com/ddohler/gdal-js
Amazon Web Services. Amazon API Gateway [EB/OL]. Seattle: Amazon Web Services. (n.d.) [2023-05-23]. https://aws.amazon.com/cn/api-gateway/
CNCF. WebAssembly Serverless Functions in AWS Lambda [EB/OL]. Place unknown: CNCF. (2021, August 25) [2023-05-23]. https://www.cncf.io/blog/2021/08/25/webassembly-serverless-functions-in-aws-lambda/
Amazon Web Services. Amazon DynamoDB – 高可靠性、高可扩展性、高性能的 NoSQL 数据库[EB/OL]. (n.d.). [2023-05-23]. https://aws.amazon.com/cn/dynamodb/.
Amazon Web Services. Amazon Cognito – 用户身份验证、注册和登录[EB/OL]. (n.d.). [2023-05-23].https://aws.amazon.com/cognito/.
Amazon Web Services. AWS Amplify – 快速构建移动和 Web 应用程序 [EB/OL]. Seattle: Amazon Web Services. (n.d.) [2023-05-23]. https://aws.amazon.com/amplify/
Amazon Web Services. Amazon CloudWatch – 监控资源和应用程序，收集和跟踪指标、收集和搜索日志，并设置警报[EB/OL]. (n.d.). [2023-05-23]. https://aws.amazon.com/cn/cloudwatch/.
Amazon Web Services. Amazon S3 – 可扩展的对象存储，可用于存储和检索任何数量和类型的数据[EB/OL]. (n.d.). [2023-05-23]. https://aws.amazon.com/cn/s3/.
Amazon Web Services. AWS CodePipeline – 连接和自动化软件发布过程[EB/OL]. (n.d.). [2023-05-23]. https://aws.amazon.com/cn/codepipeline/.
Amazon Web Services. AWS Lambda 定价 – 只需按照使用付费[EB/OL]. (n.d.). [2023-05-23].https://aws.amazon.com/cn/lambda/pricing/.

Posted 2023-05-27Updated 2023-11-2728 minutes read (About 4193 words)

GitHub Copilot 背后的 AI 编码技术：如何让 GPT 更好地理解你的代码

AI 编码工具正在逐渐改变我们的编程习惯和体验，GitHub Copilot 是这一变革的最佳代表。这款产品利用强大的算法，根据开发者的上下文和需求，从多个来源挑选出最相关的代码片段和注释，进而生成编码建议。在这篇文章中，我们将深入探讨 GitHub Copilot 背后的技术思路，结合通过逆向工程获取的部分 copilot prompt，希望能为构建 AI 辅助的编码工具提供一些帮助。这里的内容部分翻译整理自微软的博客，我们也会讨论其他人的研究成果和观点。

GitHub Copilot 通过算法从多个来源选择相关代码片段或注释，并使用上下文理解能力生成编码建议。GitHub Copilot 创建了精巧的提示词工程的方案，并在提示库中优先处理有关开发人员上下文的信息，使用向量数据库为在私有存储库中或处理专有代码的开发人员创建了定制化的编码体验。

为了让使用 GitHub Copilot 的开发人员感觉像是与另一个程序员合作，GitHub的机器学习专家一直在研究、开发和测试新功能，其中很多都集中在提高 AI 程序员的上下文理解能力。这是因为良好的交流对于合作编程至关重要，推断上下文对于实现良好的交流至关重要。

为了揭示这些背后的工作，原文作者向 GitHub 的研究员和工程师询问了他们正在做的帮助 GitHub Copilot 提高上下文理解能力的工作。以下是他们发现的内容。

从OpenAI的Codex模型到GitHub Copilot

当OpenAI在2020年6月发布GPT-3时，GitHub 知道开发人员将从专门为编码利用该模型的产品中受益。因此，他们向 OpenAI 提供输入，帮助其构建 Codex，它是GPT-3和LLM的后代，将驱动GitHub Copilot。这款程序员配对工具于2021年6月发布为技术预览版，并于2022年6月成为世界上第一个大规模生成式AI编码工具。

为确保该模型具有最佳信息，以便快速做出最佳预测，GitHub的机器学习（ML）研究员进行了大量称为提示工程的工作（将在下面详细解释），以便模型提供上下文相关的响应，并具有低延迟。

尽管GitHub总是在尝试新模型，但Codex是第一个真正强大的生成式AI模型，也是可用的，GitHub的机器学习工程师David Slater表示：“我们从模型和提示改进的迭代中获得的实践经验是非常宝贵的。”

所有这些实验最终导致了一款 pair programming 工具，最终“释放了开发人员的时间，让他们专注于更有意义的工作”。该工具甚至对于从头开始启动新项目或文件也是一个巨大的帮助，因为它提供了一个开发人员可以根据需要进行调整和改进的起点。GitHub的机器学习研究员Alice Li表示。

为什么上下文很重要

开发人员使用拉取请求、项目文件夹、开放问题等详细信息来确定其代码的上下文。当涉及到生成AI编码工具时，Copilot 需要教这个工具使用哪些信息来做同样的事情。

Transformer LLMs 擅长连接和大局思考。生成AI 编码工具是由大型语言模型（LLMs）所支持。这些模型是在大量代码和人类语言上训练的算法集。今天的最先进的 LLMs 是 transformer ，这使它们能够在用户输入的文本和模型已经生成的输出之间建立联系,这就是为什么今天的生成AI工具提供比之前的AI模型更具上下文相关性的响应。

但是，AI 需要被告知哪些信息与您的代码相关。目前，足够快速以支持GitHub Copilot的 transformer 每次只能处理大约6,000个字符。虽然这已足以推进和加速代码完成和代码更改总结等任务，但有限的字符数量意味着无法使用开发人员的所有代码作为上下文。

因此，Copilot 的挑战是找出不仅要向模型提供哪些数据，还要如何最好地排序和输入它以获得最佳建议。

GitHub Copilot 如何理解您的代码

一切都归结于提示，这些提示是集成IDE代码和相关上下文的编译，供模型使用。提示由后台算法生成，可以在您编码的任何时候生成编码建议。这就是为什么GitHub Copilot会生成编码建议，无论您是正在编写还是刚刚完成注释，或者正在处理一些复杂的代码。

下面是提示的创建过程：首先，一系列算法从当前文件和其他来源中选择相关代码片段或注释。然后，对这些片段和注释进行优先排序，过滤和组装，形成最终的提示。

GitHub Copilot的上下文理解能力不断成熟。第一个版本只能认为您在IDE中工作的文件与上下文相关。但 Copilot 团队知道上下文超出了这个范围。现在，仅仅一年后，他们正在尝试使用算法来考虑您的整个代码库，以生成定制的建议。

他们如何到达这里的：

提示工程是创建提示的精细艺术，以便模型为用户提供最有用的预测。提示告诉包括GitHub Copilot在内的LLMs，要处理哪些数据，以及以什么顺序来对您的代码进行上下文化。大部分工作都在所谓的提示库中进行，这是专家与算法一起提取和优先处理有关开发人员上下文的各种信息的地方，创建将由GitHub Copilot模型处理的提示。
相邻选项卡是称之为允许GitHub Copilot处理开发人员IDE中打开的所有文件的技术，而不仅仅是开发人员正在处理的单个文件的技术。通过打开与其项目相关的所有文件，开发人员自动调用GitHub Copilot来扫描所有数据，并在其光标周围的代码之间找到匹配的代码片段，并将这些匹配项添加到提示中。

开发相邻选项卡时，GitHub Next团队和内部ML研究人员进行了A/B测试，以确定识别IDE中代码和打开选项卡中代码之间匹配的最佳参数。他们发现设置非常低的门槛来包括匹配实际上会提供最佳的编码建议。

通过包含每一个小的上下文，相邻选项卡帮助相对增加了5%的用户接受GitHub Copilot的建议。

Fill-In-the-Middle（FIM）范式进一步扩大了上下文孔径。在FIM之前，只有光标之前的代码会被放入提示中，而忽略了光标之后的代码。（在GitHub上，将光标之前的代码称为前缀，将光标之后的代码称为后缀）。使用FIM，我们可以告诉模型提示的哪一部分是前缀，哪一部分是后缀。

即使您从头开始创建文件，并且只有文件的框架，Copilot 也知道编码不是线性或顺序的。因此，当您在文件中跳来跳去时，FIM可以帮助GitHub Copilot为您的文件中光标所在的部分或前缀和后缀之间应该出现的代码提供更好的编码建议。

基于A/B测试，FIM提高了10%的相对性能，这意味着开发人员接受了他们所看到的建议中的10%以上。由于最佳的缓存使用，相邻选项卡和FIM在后台运行，不会增加任何延迟。

也许结合实际的代码来理解会更好一些。例如，在逆向出来的 Github Copilot 插件代码中，在构建 prompt 时包含了以下的内容：

exports.Priorities =
  exports.PromptWishlist =
  exports.PromptElementRanges =
  exports.PromptChoices =
  exports.PromptBackground =
  exports.PromptElementKind =
    undefined;
const M_prompt_parsing_utils_maybe = require("prompt-parsing-utils");
const M_tokenizer_maybe = require("tokenizer");
var i;
!(function (e) {
  e.BeforeCursor = "BeforeCursor";
  e.AfterCursor = "AfterCursor";
  e.SimilarFile = "SimilarFile";
  e.ImportedFile = "ImportedFile";
  e.LanguageMarker = "LanguageMarker";
  e.PathMarker = "PathMarker";
})((i = exports.PromptElementKind || (exports.PromptElementKind = {})));

这段代码的主要作用是定义了一种枚举类型，用于表示 GitHub Copilot 系统内部使用的各种提示元素类型，并导入了一些可能与这些提示元素处理相关的模块。它定义了一些名为 PromptElementKind 的变量，该变量是一个枚举对象，用于描述不同类型的提示元素。提示元素可能是在编码过程中需要的不同种类的信息，例如光标之前或之后的代码、相似的文件、已导入的文件、语言标记和路径标记。这些提示可能包括从当前文件和其他来源选择的相关代码片段或注释，然后对这些片段和注释进行优先排序、过滤和组装，形成最终的提示。这些提示告诉模型处理哪些数据，以及以什么顺序来对代码进行上下文化。

一个实际的 Copilot 的提示的示例可能是这样的：

{
  "prefix": "# Path: codeviz\\\\app.py\\n# Compare this snippet from codeviz\\\\predictions.py:\\n# import json\\n# import sys\\n# import time\\n# from manifest import Manifest\\n# \\n# sys.path.append(__file__ + \\"/..\\")\\n# from common import module_codes, module_deps, module_categories, data_dir, cur_dir\\n# \\n# gold_annots = json.loads(open(data_dir / \\"gold_annotations.js\\").read()",
  "suffix": "if __name__ == '__main__':\\r\\n    app.run(debug=True)",
  "isFimEnabled": true,
  "promptElementRanges": [
    { "kind": "PathMarker", "start": 0, "end": 23 },
    { "kind": "SimilarFile", "start": 23, "end": 2219 },
    { "kind": "BeforeCursor", "start": 2219, "end": 3142 }
  ]
}

正如您所见，此提示包括前缀和后缀。然后，Copilot将此提示（经过一些格式化）发送到模型。在这种情况下，Copilot正在以“插入模式”（也称为填写中间（FIM）模式）调用 Codex，因为后缀不为空。

提高语义理解能力

今天，Copilot 正在尝试使用向量数据库，可以为在私有存储库中或处理专有代码的开发人员创建定制编码体验。生成式AI编码工具使用称为嵌入的东西从向量数据库中检索信息。

什么是向量数据库？ 它是一个索引高维向量的数据库。
什么是高维向量？ 它们是对象的数学表示，因为这些向量可以以多个维度模拟对象，所以它们可以捕捉该对象的复杂性。当适当地用于表示代码片段时，它们可以表示代码的语义甚至意图，而不仅仅是语法。
什么是嵌入？ 在编码和LLM的上下文中，嵌入是将代码片段表示为高维向量的方式。由于LLM对编程和自然语言的“知识”，它能够在向量中捕捉代码的语法和语义。

以下是它们如何共同运作的方式：

算法将为存储库中的所有片段（可能是数十亿个）创建嵌入，并将其存储在向量数据库中。
然后，当您编码时，算法会在IDE中嵌入片段。
算法随后会在嵌入到IDE片段和已存储在向量数据库中的嵌入之间进行近似匹配，也是实时的。向量数据库是使算法能够快速搜索向量上的近似匹配（而不仅仅是精确匹配），即使它存储了数十亿个嵌入的原因。

开发人员熟悉使用哈希码检索数据，这通常会寻找精确的字符匹配，GitHub的高级ML研究员Alireza Goudarzi解释说。“但嵌入——因为它们来自于经过大量数据培训的LLM——会在代码片段和自然语言提示之间建立语义上的接近感。”

阅读以下三个句子，并确定哪两个语义最相似。

句子A：国王移动并俘获了兵。
句子B：国王在威斯敏斯特大教堂加冕。
句子C：两个白色的战车仍然在比赛中。

答案是句子A和C，因为两者都是关于国际象棋的。虽然句子A和B在语法上或结构上相似，因为国王是主语，但它们在语义上是不同的，因为“国王”在不同的上下文中使用。

以下是每个语句如何转换为Python。请注意，尽管它们在语义上不同，但片段A和B之间具有语法上的相似性，而片段A和C之间具有语义上的相似性。

片段A：

1
2
3

if king.location() == pawn.location():
board.captures_piece(king, pawn)

片段B：

1
2
3

if king.location() == "Westminster Abbey":
king.crown()

片段C：

1
2
3

if len([ r for r in board.pieces("white") if r.type == "rook" ]) == 2:
return True

如上所述，Copilot 仍在尝试检索算法，并正在为企业客户设计该功能，特别是那些正在寻找定制编码体验的私有存储库，并明确选择使用该功能。

我们可以进一步结合逆向工程的 copilot 代码讨论这个问题。为了处理大规模的自然语言处理任务， Copilot 在客户端使用了 Cushman + ONNX 模型处理。具体来说，Copilot 将 Cushman 模型的输出转换为向量表示，然后使用向量相似度计算来匹配最相关的本地文件。

除了就地矢量化（Vector）与相似度匹配，Copilot 还使用了本地的相似计算与 token 处理来管理 token，以便更好地处理大规模自然语言处理任务。例如，在 Copilot 逆向工程中出现的可能的代码片段如下：

e.prototype.useAutoCorrelation = function (e, t) {
    if (e && !this._isAutoCorrelating) {
      M_correlation_context_manager.CorrelationContextManager.enable(t);
    } else {
      if (!e && this._isAutoCorrelating) {
        M_correlation_context_manager.CorrelationContextManager.disable();
      }
    }
    this._isAutoCorrelating = e;
  };

总结与回顾

去年，Copilot 团队对 GitHub Copilot 进行了定量研究，发现使用这个软件的开发者能够以高达 55% 的速度编码。这意味着开发者感到更加高效，能够更快地完成重复性任务，并且能够更专注于令人满意的工作。但是我们的工作不会止步于此。

GitHub 产品和研发团队，包括 GitHub Next，一直在与 Microsoft Azure AI 平台合作，继续改进 GitHub Copilot 的上下文理解。许多帮助 GitHub Copilot 理解您的代码的工作都是在幕后进行的。当您编写和编辑您的代码时，GitHub Copilot 会实时响应您的写作和编辑，通过生成提示（或者说，基于您在 IDE 中的操作，优先排序并发送相关信息给模型）来不断给出最佳编码建议。

了解更多

GitHub Copilot X 是对于以 AI 为动力的软件开发的未来设想。发现新内容。
了解支持 GitHub Copilot 的 LLMs 如何变得更加优秀。
阅读对应的研究，了解 GitHub Copilot 如何影响开发者的生产力。

Copilot 逆向工程相关资料：

Posted 2023-05-14Updated 2023-11-2722 minutes read (About 3270 words)

ChatGPT 插件开发者教程与最佳实践 - 快速上手开发 plugins

我这两天也用上了 ChatGPT 的插件，感觉还是挺好玩的（也许是被 Google 的 AI 和微软逼出来的吧），开发一个插件实际上一点也不难，出乎意料地简单。

本文介绍了如何使用 OpenAPI 规范记录 API，以及如何将插件连接到ChatGPT UI。同时，还提供了编写插件描述和调试插件的最佳实践。通过定义 OpenAPI 规范以及清单文件，可以来创建一个待办事项列表插件。这里还有基于 Vercel 平台的开发者模板，可以帮助您轻松开发和部署 ChatGPT 插件，并一键上线使用：https://github.com/yunwei37/ChatGPT-plugin-vercel-template 。

本文部分整理自 OpenAI 的官方文档。

创建插件需要3个步骤：

构建API
以OpenAPI yaml或JSON格式文档化API
创建一个JSON清单文件，用于为插件定义相关元数据

本节的重点将是通过定义OpenAPI规范以及清单文件来创建一个待办事项列表插件。

可以在 OpenAI 的仓库中浏览示例插件，涵盖多种用例和身份验证方法。

插件清单

每个插件都需要一个ai-plugin.json文件，它需要托管在 API 的域中。

例如，名为example.com 的公司将通过 https://example.com 域使插件JSON文件可访问，因为它们的API被托管在该域中。当您通过ChatGPT UI安装插件时，在后端我们会查找位于/.well-known/ai-plugin.json的文件。/.well-known文件夹是必需的，并且必须存在于您的域中，以便ChatGPT与您的插件连接。如果找不到文件，则无法安装插件。对于本地开发，您可以使用HTTP，但如果指向远程服务器，则需要使用HTTPS。

所需的ai-plugin.json 文件的最小定义如下：

{
    "schema_version": "v1",
    "name_for_human": "TODO Plugin",
    "name_for_model": "todo",
    "description_for_human": "Plugin for managing a TODO list. You can add, remove and view your TODOs.",
    "description_for_model": "Plugin for managing a TODO list. You can add, remove and view your TODOs.",
    "auth": {
        "type": "none"
    },
    "api": {
        "type": "openapi",
        "url": "http://localhost:3333/openapi.yaml",
        "is_user_authenticated": false
    },
    "logo_url": "http://localhost:3333/logo.png",
    "contact_email": "[email protected]",
    "legal_info_url": "http://www.example.com/legal"
}

如果您想查看插件文件的所有可能选项，请参考以下定义。在命名插件时，请牢记我们的插件指南，不遵守这些指南的插件将不会被批准放入插件商店。

Field	Type	Description / Options	Required
schema_version	String	Manifest schema version	✅
name_for_model	String	Name the model will use to target the plugin (no spaces allowed, only letters and numbers). 50 character max.	✅
name_for_human	String	Human-readable name, such as the full company name. 20 character max.	✅
description_for_model	String	Description better tailored to the model, such as token context length considerations or keyword usage for improved plugin prompting. 8,000 character max.	✅
description_for_human	String	Human-readable description of the plugin. 100 character max.	✅
auth	ManifestAuth	Authentication schema	✅
api	Object	API specification	✅
logo_url	String	URL used to fetch the logo. Suggested size: 512 x 512. Transparent backgrounds are supported.	✅
contact_email	String	Email contact for safety/moderation, support, and deactivation	✅
legal_info_url	String	Redirect URL for users to view plugin information	✅
HttpAuthorizationType	HttpAuthorizationType	“bearer” or “basic”	✅
ManifestAuthType	ManifestAuthType	“none”, “user_http”, “service_http”, or “oauth”

interface BaseManifestAuth	BaseManifestAuth	type: ManifestAuthType; instructions: string;

ManifestNoAuth	ManifestNoAuth	No authentication required: BaseManifestAuth & { type: ‘none’, }

ManifestAuth	ManifestAuth	ManifestNoAuth, ManifestServiceHttpAuth, ManifestUserHttpAuth, ManifestOAuthAuth

以下是使用不同身份验证方法的示例：

# App-level API keys
type ManifestServiceHttpAuth  = BaseManifestAuth & {
  type: 'service_http';
  authorization_type: HttpAuthorizationType;
  verification_tokens: {
    [service: string]?: string;
  };
}

# User-level HTTP authentication
type ManifestUserHttpAuth  = BaseManifestAuth & {
  type: 'user_http';
  authorization_type: HttpAuthorizationType;
}

type ManifestOAuthAuth  = BaseManifestAuth & {
  type: 'oauth';

  # OAuth URL where a user is directed to for the OAuth authentication flow to begin.
  client_url: string;

  # OAuth scopes required to accomplish operations on the user's behalf.
  scope: string;

  # Endpoint used to exchange OAuth code with access token.
  authorization_url: string;

  # When exchanging OAuth code with access token, the expected header 'content-type'. For example: 'content-type: application/json'
  authorization_content_type: string;

  # When registering the OAuth client ID and secrets, the plugin service will surface a unique token.
  verification_tokens: {
    [service: string]?: string;
  };
}

上述清单文件中某些字段的长度有限制，这些限制可能会发生变化。我们还对 API 响应正文强制实施 10 万字符的最大值，这个值也可能会随时间变化而改变。

总的来说，最佳实践是尽可能简洁地描述和响应，因为模型有限的上下文窗口。

OpenAPI 定义

下一步是构建 OpenAPI规范来记录API。ChatGPT模型除了OpenAPI规范和清单文件中定义的内容之外，不知道关于您的API的任何信息。这意味着如果您有一个广泛的API，您不需要将所有功能暴露给模型，可以选择特定的端点。例如，如果您有一个社交媒体API，您可能希望让模型通过GET请求访问站点内容，但防止模型能够评论用户的帖子，以减少垃圾邮件的机会。

OpenAPI规范是包装在您的API之上的外壳。基本的OpenAPI规范将如下所示：

openapi: 3.0.1
info:
  title: TODO Plugin
  description: A plugin that allows the user to create and manage a TODO list using ChatGPT.
  version: 'v1'
servers:
  - url: http://localhost:3333
paths:
  /todos:
    get:
      operationId: getTodos
      summary: Get the list of todos
      responses:
        "200":
          description: OK
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/getTodosResponse'
components:
  schemas:
    getTodosResponse:
      type: object
      properties:
        todos:
          type: array
          items:
            type: string
          description: The list of todos.

我们首先定义规范版本、标题、描述和版本号。当在 ChatGPT 中运行查询时，它将查看在信息部分中定义的描述，以确定插件是否与用户查询相关。您可以在编写描述部分了解更多提示信息。

请记住以下 OpenAPI 规范的限制，这些限制可能会发生变化：

API 规范中每个 API 端点描述 / 摘要字段的最大字符数为200个字符
API规范中每个API参数描述字段的最大字符数为200个字符

由于我们正在本地运行此示例，因此我们希望将服务器设置为指向您的本地主机 URL 。其余的 OpenAPI 规范遵循传统的 OpenAPI 格式，您可以通过各种在线资源了解有关OpenAPI格式的更多信息。还有许多工具可以根据您的基础 API 代码自动生成 OpenAPI 规范。

运行插件

创建API、清单文件和OpenAPI规范之后，您现在可以通过ChatGPT UI连接插件。您的插件可能在本地开发环境或远程服务器上运行。

如果您有一个本地版本的API正在运行，您可以将插件界面指向您的本地主机。要将插件与ChatGPT连接，请导航到插件商店并选择“开发您自己的插件”。输入您的本地主机和端口号（例如localhost:3333）。请注意，目前仅支持none认证类型进行本地主机开发。

如果插件正在远程服务器上运行，则需要首先选择“开发您自己的插件”进行设置，然后选择“安装未经验证的插件”进行安装。您只需将插件清单文件添加到yourdomain.com/.well-known/路径并开始测试API即可。但是，对于清单文件的后续更改，您将不得不将新更改部署到公共站点上，这可能需要很长时间。在这种情况下，我们建议设置本地服务器以充当API的代理。这样，您可以快速原型化OpenAPI规范和清单文件的更改。

编写插件描述

当用户提出一个可能是插件请求的查询时，模型会查看OpenAPI规范中端点的描述以及清单文件中的“description_for_model”。与提示其他语言模型一样，您需要尝试多个提示和描述，以查看哪个效果最好。

OpenAPI规范本身是提供有关API各种细节的好地方，例如可用的功能以及其参数等。除了为每个字段使用富有表现力的、信息丰富的名称外，规范还可以针对每个属性包含“描述”字段。这些描述可用于提供自然语言描述，例如功能的作用或查询字段期望的信息。模型将能够看到这些描述，并指导其使用API。如果某个字段仅限于某些值，您还可以提供具有描述性类别名称的“枚举”。

“description_for_model”属性为您提供了自由，使您可以指示模型通常如何使用您的插件。总的来说，ChatGPT背后的语言模型非常擅长理解自然语言并遵循指示。因此，这是一个很好的地方，可以放置有关您的插件的一般说明以及模型应如何正确使用它的说明。使用自然语言，最好是简洁而又描述性和客观的语气。您可以查看一些示例，以了解这应该是什么样子。我们建议用“Plugin for…”开头，然后列出您的API提供的所有功能。

最佳实践

以下是编写description_for_model和OpenAPI规范中的描述以及设计API响应时应遵循的最佳实践：

描述不应尝试控制ChatGPT的情绪、个性或确切的响应。ChatGPT的设计目的是编写适当的插件响应。

不良示例:

当用户要查看待办事项清单时，总是回复“我能找到您的待办事项清单！您有[x]个待办事项：[列出待办事项]。如果您想要，我可以添加更多待办事项！”

良好示例:

[不需要提供描述]
描述不应鼓励ChatGPT在用户未要求使用插件的特定服务类别时使用插件。

不良示例:

每当用户提到任何类型的任务或计划时，都要问他们是否想要使用 TODO 插件将某些内容添加到他们的待办事项清单中。

良好示例:

TODO 列表可以添加、删除和查看用户的待办事项。
描述不应规定 ChatGPT 使用插件的具体触发器。ChatGPT 的设计是在适当时自动使用插件。

不良示例:

当用户提到任务时，请回复：“您是否希望我将此添加到您的待办事项清单中？说 ‘是’ 继续。”

良好示例:

[不需要提供描述]

插件 API 响应应返回原始数据而不是自然语言响应，除非必要。ChatGPT 将使用返回的数据提供自己的自然语言响应。

不良示例:

我能找到您的待办事项清单！您有2个待办事项：买东西和遛狗。如果您想要，我可以添加更多待办事项！

良好示例:

{“todos”: [“买东西”, “遛狗”]}

调试插件

默认情况下，聊天不会显示插件调用和未向用户显示的其他信息。为了更全面地了解模型与您的插件的交互方式，您可以在与插件交互后单击插件名称后面的向下箭头以查看请求和响应。

模型对插件的调用通常包括来自模型的包含 JSON 类参数的消息，这些参数被发送到插件，随后是插件的响应，最后是模型利用插件返回的信息发送的消息。

如果您正在开发一个本地主机插件，您还可以通过转到“设置”并切换“打开插件开发工具”来打开开发人员控制台。从那里，您可以看到更详细的日志和 “刷新插件” ，它会重新获取插件和OpenAPI规范。

本文介绍了如何使用OpenAPI规范记录API，以及如何将插件连接到ChatGPT UI。同时，还提供了编写插件描述和调试插件的最佳实践。OpenAPI规范包括版本、标题、描述和版本号等基本信息，还可以为每个属性提供自然语言描述，例如功能的作用或查询字段期望的信息。调试插件可以通过向下箭头查看请求和响应，或通过开发人员控制台查看更详细的日志。

开发模板

这里还有一个基于 Vercel 平台的 ChatGPT 插件起始模板，可以帮助您轻松地部署 ChatGPT 插件，并实现一键上线服务：https://github.com/yunwei37/ChatGPT-plugin-vercel-template

点击原文链接即可查看。

参考资料

Posted 2023-05-14Updated 2023-11-2728 minutes read (About 4221 words)

WebAssembly 组件模型详解

本文部分翻译自 fermyon 的一篇博客，原文地址： https://www.fermyon.com/blog/webassembly-component-model
对于一种语言生态而言，标准可能并不是其中最令人激动的部分。但是，“组件模型” 这个看似无聊的名称背后，是Wasm为软件世界带来的最重要的创新。组件模型正在快速发展，并且已经有了参考实现，2023 年很可能是组件模型开始重新定义我们如何编写软件的一年。

WebAssembly 组件模型是一个提案，旨在通过定义模块在应用程序或库中如何组合来构建核心 WebAssembly 标准。正在开发该模型的存储库包括非正式规范和相关文档，但是这种详细程度可能会一开始让人有些不知所措。

在本文中，我们首先简要解释组件模型的动因。然后，我们将建立对其工作方式的直觉，并将其与流行操作系统（如Windows、macOS和Linux）上的本地代码链接和运行进行比较。本文的目标受众是已经熟悉本地编译语言（如C、Rust和Go）以及动态链接和进程间通信等概念的开发人员。在下一个部分中，我们讨论一下 eunomia-bpf 社区在组件模型上的一些实践工作，并介绍一种名为WIT（Wasm Interface Type）的文档格式，用于描述组件模型接口的方式。

动机

WebAssembly规范定义了一种体系结构、平台和语言无关的可执行代码格式。WebAssembly模块可以从主机运行时导入函数、全局变量等，也可以将这些项导出到主机。然而，在运行时没有标准的方式来合并模块，也没有标准的方式来跨模块边界传递高级类型（例如字符串和记录）。

实际上，缺乏模块组合意味着模块必须在构建时静态链接，而不能在运行时动态链接，并且它们不能以标准、便携的方式与其他模块通信。组件模型通过在核心WebAssembly之上提供以下三个主要功能来解决这个问题：

接口类型：一种语言无关的方式，用于基于高级类型（如字符串、记录、集合等）定义模块接口。
规范ABI，它指定高级类型如何以核心WebAssembly的低级类型来表示。
模块和组件链接：一种动态组合模块成为组件的机制。这些组件本身可以组合在一起形成更高级的组件。

这些功能共同允许在没有静态链接的重复和安全漏洞的情况下打包和重用代码。这种重用特别适用于多租户云计算，其中成千上万个模块的代码重复会增加昂贵的存储和内存开销。

本地代码类比

如果您熟悉本地代码的链接和执行方式，那么您就会遇到“可执行文件”、“进程”和“共享库”等概念。组件模型具有相似的概念，但使用不同的术语。在这里，我们将为每个本地代码概念匹配其WebAssembly对应物，并考虑它们的相似之处和不同之处。

组件 <-> 可执行文件

Wasm组件就像本地可执行文件一样：惰性且无状态，等待使用。

模块 <-> 共享库

Wasm模块就像共享库（例如.dll、.dylib或.so），可以导出和/或导入符号，以便与其他代码链接在一起。与组件一样，模块是惰性且无状态的，等待使用。

组件实例 <-> 进程

组件的_实例_就像进程；它是组件的加载和运行形式；它是有状态和动态的。像进程一样，几个组件实例可以组织成树，以便每个节点都可以与其直接子节点通信。与进程一样，组件实例之间不共享内存或其他资源，必须通过某种主机介入方式进行通信。

请注意，可以从同一可执行文件运行多个进程-有时同时运行-而这些进程不共享状态。同样，从同一组件产生的实例不共享状态。

模块实例 <-> 已加载的共享库

模块的_实例_就像已加载和链接到进程中的库一样。它是有状态和动态的，与组件的其他部分共享内存和其他资源。

请注意，一个给定的模块可以同时实例化到多个组件中，这些实例之间_不会_共享状态。

一些共享库也可以是可执行文件；即它们可以被链接到进程或作为独立进程执行。同样，Wasm模块实例可以链接到组件实例中或由主机运行时独立运行。

Wasm运行时 <-> 操作系统

Wasm运行时（例如wasmtime）类似于操作系统，它负责加载和链接组件（即进程）并在它们之间进行通信。

然而，与大多数提供少量低级进程间通信方法的操作系统不同（例如管道、stdin/stdout等），启用组件的Wasm运行时提供了一种基于接口类型和规范ABI的单一高级通信方法。此方法类似于诸如gRPC的RPC协议，但它旨在（并优化）用于本地通信，而不是通过网络。

对于跨模块边界的组件内通信，组件模型没有指定标准的ABI。这意味着要在组件内链接的模块必须就适当的ABI达成一致，这可以是特定于语言的或与语言无关的。

与本地模型相反，其中进程间通信通常比库调用更麻烦和复杂，组件模型旨在使组件间和模块间通信都方便和表达。结论是，您可以将Wasm应用程序分成多个单独的沙盒组件，而不需要比共享同一个沙盒的模块更多的工作。

注意事项

以上讨论为简单起见忽略了一些细微差别和例外。例如，流行操作系统上的进程_可以_共享内存、文件句柄等，尽管它们通常不这样做。同样，未来的 WASI API 可能会允许组件实例之间进行类似的共享。

同样，组件可能有除上述 ABI 之外的其他通信方式：网络套接字、文件、JavaScript 环境等。具体细节取决于主机运行时所支持的和授予每个组件的功能。

（借用的）可视化

以下图示托管在组件模型存储库，展示了 Wasm 模块和组件的静态和动态链接，右侧的图示表示加载到组件实例中的模块实例。不过，它同样可以展示本地的静态和动态链接，右侧的图示表示进程及其加载的库。

结论

虽然组件模型相对较新且仍在开发中，但它遵循了几十年来用于组织本地代码的相同模式。模块、组件及其实例化方式促进了代码重用和隔离，类似于共享库、可执行文件和进程在您喜爱的操作系统中的使用方式。

此外，组件模型通过提供可跨组件边界使用的表达力强、高级别的ABI，改进了本地模型。这使得在保持代码隔离的同时轻松重用代码，提高了安全性和可靠性。

在Fermyon，我们对组件模型感到兴奋，因为它对于使Spin微服务安全、高效和易于开发至关重要。Spin已经使用Wasmtime的强大沙盒保证来将服务彼此隔离，并使用wit-bindgen提供高级别、语言无关的API，用于常见功能，如HTTP请求。未来，我们将积极贡献于Wasmtime和其他项目，以帮助实现组件支持，并在它们稳定后采用关键功能用于 Spin。

在下一个部分中，我们希望讨论一下 eunomia-bpf 社区在组件模型上面的一些实践工作。eunomia-bpf 社区正在探索 eBPF 和 WebAssembly 相互结合的工具链和运行时: https://github.com/eunomia-bpf/wasm-bpf 。社区关注于简化 eBPF 程序的编写、分发和动态加载流程，以及探索 eBPF 和 Wasm 相结合的工具链、运行时和运用场景等技术。

组件模型的描述文件 - WIT

由于Wasm组件提供了导入和导出“接口”的功能，因此我们可以使用一种称为WIT（Wasm Interface Type）的文档格式来描述这种接口。Wasm接口类型（WIT）格式是一种IDL（接口描述语言），用于以两种主要方式为WebAssembly组件模型提供工具支持：

WIT是一种开发者友好的格式，用于描述组件的导入和导出。易于阅读和编写，并为从客户语言生成组件以及在主机语言中使用组件提供基础。
WIT包是在组件生态系统中共享类型和定义的基础。作者可以从其他WIT包导入类型，生成组件，发布代表主机嵌入的WIT包，或协作定义跨平台共享API的WIT定义。

WIT包是WIT文档的集合。每个WIT文档都定义在一个使用文件扩展名wit的文件中，例如foo.wit，并编码为有效的UTF-8字节。每个WIT文档包含一个接口和世界的集合。类型可以从包内的同级文档（文件）中导入，还可以通过URL从其他包中导入。

简单来说，WIT文件描述了Wasm组件的导入和导出以及其他相关信息，包括：

导入和导出的函数
导入和导出的接口
用于上述函数和接口的参数或返回值的类型，包括record（类似于结构体）、variant（类似于Rust的enum，一种tagged union）、union（类似于C的union，untagged union）、enum（类似于C的enum，映射到整数）等。

有关类型的更详细信息，请参见https://github.com/WebAssembly/component-model/blob/main/design/mvp/WIT.md#wit-types

以下是一个WIT文档的示例，其中描述了：

一个名为my-world的world。可以认为一个world对应一个Wasm组件。
组件内导出了一个名为run的函数，该函数不接受任何参数，也没有返回值。
组件需要导入一个名为host的接口，其需要提供一个名为log的函数，并接收一个名为param的字符串参数。

default world my-world {
  import host: interface {
    log: func(param: string)
  }
  export run: func()
}

如何在实际项目中使用 WIT 开发 Wasm 组件

鉴于组件模型和 WIT 已经如此出色，那么我们该如何使用它们呢？

BytecodeAlliance 开发了 wit-bindgen 和 wasm-tools 两个工具，可以帮助我们生成处理接口、字符串、数组、结构体等复杂类型的代码，而我们只需要关心具体函数的实现即可。
使用传统的 Wasm 工具链（如 clang、rustc）编译生成 Wasm 模块后，再将其转换成 Wasm 组件。

以本文提供的示例为例，将其保存为 test.wit 文件后，使用 wit-bindgen c test.wit -w test.my-world 命令即可生成面向 C 程序的 binding，即以下三个文件：

my-world.h，其中包含了我们写的组件从外部导入的函数的声明（host 接口下的 log 函数），以及我们需要自己编写的函数的声明（run 函数）。
my-world.c，其中包含了一些工具函数的实现，例如操作组件模型中的字符串类型的工具函数。
my_world_component_type.o，包含了几个工具 section，用于 wasm-tools 工具将模块转换为组件。我们需要将此文件链接到我们的目标文件中。

my-world.h 的内容请参考以下示例：

#ifndef __BINDINGS_MY_WORLD_H
#define __BINDINGS_MY_WORLD_H
#ifdef __cplusplus
extern "C" {
#endif#include <stdlib.h>#include <string.h>#include <stdint.h>#include <stdbool.h>typedef struct {
  char*ptr;
  size_t len;
} my_world_string_t;

// Imported Functions from `host`void host_log(my_world_string_t *param);
// Exported Functions from `my-world`void my_world_run(void);
// Helper Functionsvoid my_world_string_set(my_world_string_t *ret, const char*s);
void my_world_string_dup(my_world_string_t *ret, const char*s);
void my_world_string_free(my_world_string_t *ret);

#ifdef __cplusplus
}
#endif#endif

示例

不同语言编写的 Wasm 组件协同工作

我们在这个例子中展示了通过wit-bindgen分别用C和Rust来编写组件，并且让他们互相调用，然后在wasmtime这个支持组件模型的Wasm运行时上运行。

https://github.com/eunomia-bpf/c-rust-component-test

btf2wit

一个从BTF（BPF Type Format，一种让eBPF程序在内核中根据不同版本进行重定位的调试信息）生成 WIT 描述文件的小工具，用于使用 Wasm 进行 eBPF 用户态程序的开发

https://github.com/eunomia-bpf/btf2wit

Rust + wit-bingen

一个用 Rust 编写 eBPF 程序并编译为 Wasm 运行，并使用 btf2wit 生成内核结构体的WIT定义在用户态解析数据的例子：

https://github.com/eunomia-bpf/wasm-bpf/tree/main/examples/rust-bootstrap

关于WIT和组件模型的更多信息

截止至 2023 年 3 月，组件模型现在还很不成熟，目前为止没有任何一个完整支持组件模型的Wasm运行时。
但wasmtime现在对组件模型提供初步支持（虽然一堆bug），也因此上面的例子用的是wasmtime。
关于WASI。现在已经有了组件模型使用WASI的标准（preview2），但目前为止没有任何运行时实现了这个标准。所以暂时组件模型里用不了WASI。

参考资料

https://github.com/WebAssembly/component-model https://github.com/WebAssembly/component-model
*2023 年 WebAssembly 技术五大趋势预测* https://zhuanlan.zhihu.com/p/597705400
webassembly-component-model https://www.fermyon.com/blog/webassembly-component-model
*Wasm-bpf: 为云原生 Webassembly 提供通用的 eBPF 内核可编程能力*https://www.infoq.cn/article/sXrpXdGOTAUW6XWRcKRx

Posted 2023-05-14Updated 2023-11-275 minutes read (About 767 words)

AI 插件：未来的浏览器、前端与交互

想象一下，你在浏览器中粘贴一个 URL，这个 URL 不仅仅是一个网址，而是一个功能强大、能执行多种任务的 AI 插件。这听起来像是未来的事情，但实际上，这种变革已经悄悄进行中。

1. 插件的魅力与局限性

当我第一次接触到 ChatGPT 插件时，我被其简洁高效的设计所吸引。在我看来，插件不仅仅是一个功能扩展，它其实是未来的网络和前端的一种新形态。简单说，它就像是一个“超级浏览器”，在其中，每个插件都有其独特的功能和特色，而我们只需简单地调用它。

2. 从 UNIX 哲学到 AI 插件

UNIX 的哲学是“做一件事，做得好”。而在今天，这种哲学正在逐渐体现在 AI 插件中。想象一下，每一个 URL 都是一个功能强大的 AI agent，你不需要跳转到多个页面或下载多个应用，只需要调用相应的 AI 插件，你想要的功能就能得到实现。而随着 AI 技术的进步，这种可能性正在成为现实。

3. AI 时代的前端和交互界面

如果说以前的前端开发是构建复杂的逻辑和界面，那么在 AI 时代，这一切都将变得更加简洁。未来的前端不再是复杂的代码和交互逻辑，而是一个能与 AI 无缝对接的界面。UI 仍将存在，但其背后的逻辑将大大简化。这种变革不仅会使开发变得更加简单，也将为用户带来前所未有的体验。

4. AI 的语言：API 的重要性

在 AI 时代，API 将成为与 AI 交流的桥梁。而为了实现这一点，我们不仅需要为人类提供清晰的 API 文档，还要为 AI 提供更为详细的自然语言描述。这样，AI 就能更好地理解我们的需求，并为我们提供更精准的服务。

5. 未来的软件研发与人工智能

未来的软件研发将分为两类人：使用 AI 实现需求的人和研究 AI 的人。这意味着，我们每个人都有可能成为一个“程序员”。不再是复杂的代码和算法，只需要调用 AI，你的想法就能变为现实。

结论：

我们正在步入一个全新的 AI 时代，在这个时代中，AI 插件将彻底改变我们的上网习惯和前端开发方式。它不仅仅是一个技术的变革，更是一场思维方式的革命。而在这场革命中，每个人都有机会成为参与者和创新者。

Posted 2023-03-23Updated 2023-11-27an hour read (About 13035 words)

综述阅读：运行时软件补丁（热更新/动态更新？）分类、调查和未来方向

https://arxiv.org/pdf/2203.12132.pdf

运行时软件修补:分类、调查和未来方向

运行时软件补丁旨在最小化或消除服务停机时间、用户中断和潜在数据损失，在部署补丁时。由于现代软件系统具有高度的差异性和异构性，没有通用的解决方案可用或提出以在运行时部署和执行补丁。现有的运行时软件补丁解决方案关注特定的情况、场景、编程语言和操作系统。本文旨在识别、调查和综合最先进的运行时软件补丁方法，并概述目前未解决的挑战。它还提供了有关运行时修补方法的多个方面的见解，如修补规模、一般策略和责任。这项研究确定了七个粒度级别、两个关键策略提供了三个责任实体的概念模型，以及四个运行时修补解决方案的能力。通过对现有文献的分析，本研究还揭示了阻碍运行时修补更全面采用的开放问题。最后，它提出了几个需要更多研究人员和实践者关注的重要未来方向。

1 INTRODUCTION

现代软件不断发展和适应不断变化的用户需求和要求，这导致需要对现有软件代码应用各种变更。在传统的软件开发生命周期中，软件变更是在代码编译和部署步骤中实现的。这些变更范围从简单的错误修复到全面的软件重构。现代软件的复杂性不断增加，用户需求不断增长，导致频繁的软件修改以更新和补丁的形式提供。这种代码修改通常旨在改进或扩展现有软件功能以满足新的用户需求。改进不一定涉及核心软件系统功能，但可以专注于增强辅助属性，如安全或隐私。
补丁和更新之间的区别没有普遍接受的正式定义。然而，普遍理解是引入新功能的软件变更称为更新（或升级）。相反，修复现有错误或漏洞的小改动被称为补丁。或者，一些版本控制系统松散地将软件兼容性定义为补丁和更新之间的分界线。然而，即使是较小的错误修复补丁也可能破坏与先前版本的兼容性，使得基于兼容性的区分在实践中不足。无论使用的术语是什么，补丁和更新本质上都涉及从简单到相当复杂的代码修改。
在最简单的形式中，用更新版本替换先前运行的软件实例涉及停止旧的软件实例并启动新的实例。这样运行的软件实例可以是单个进程。

Web服务、虚拟机或容器。然而，根据软件变更的程度和类型，更新过程可能会导致长时间的软件服务停机，这可能会对终端用户的体验产生负面影响。从终端用户的角度来看，更新也可能被视为现有使用会话的中断或新会话建立的延迟。这种软件服务中断可能会在高度关键的环境中（如医疗或工业控制领域）造成严重的负面后果。此外，像大型数据中心或股票交易所这样的高负载利润导向环境可能会遭受直接的财务损失，即使是短暂的停机也可能如此。Gartner最近的一份报告表明，仅一小时的停机成本可能高达100万至500万美元。因此，开发了运行时软件修补（简称为运行时修补），也称为热修补、动态修补或在线修补。为了改善传统（也称为离线）修补，运行时软件修补旨在最小化或完全避免任何软件操作中断。运行时修补通常被认为是一种快速漏洞缓解技术。但是，与简单的传统修补（即源代码修补）相比，修补正在运行的软件会带来重大挑战。即必须实现保留现有的终端用户活动（以及与未来活动的兼容性），从人类输入到复杂的基于网络的通信会话，以实现有效的运行时修补。换句话说，软件的未来行为必须受应用程序修补的影响，当前执行的活动和使用的数据也需要相应地进行调整，以保持兼容性。在某些情况下，运行时修补会将代码注入易受攻击的程序以实现临时修复。这些临时修复旨在立即禁用或替换易受攻击的代码，以防止漏洞的利用。同时，开发人员可以实现和测试实际修复错误而不仅仅是禁用当前损坏的功能的适当更新。请注意，与修补批准、测试、签名和分发相关的其他非技术供应链要求可能会在实践中引入更多的显着修补采用延迟。采用运行时修补需要深入了解软件实现细节。例如，将现有的内部函数或对象转换为与更新的软件版本兼容需要深入了解对象格式、结构和位置。

然而，由于底层硬件、编译器、第三方库和操作系统（OS）的技术多样性，没有实现综合运行时修补机制。现有的运行时修补解决方案针对特定的领域或场景，例如物联网设备或数据中心规模的虚拟机和超级虚拟机[9-13]。这些解决方案通常专注于特定平台的挑战，例如资源受限的物联网设备固有的硬件限制。例如，即使在严格的存储限制下，存储软件的修补副本可能也是不可能的。现有的修补研究和评论没有提供定量确定修补规模的正式方法，因此在与修补和更新差异相关的术语方面存在空白。此外，由于现有的特定于平台的修补解决方案数量众多且多样化，缺乏对一般运行时修补策略和所需实现能力（如方法适用性和预期潜在干扰）的全面和正式的理解。此外，运行时修补中涉及的不同方的角色以及他们在各种修补过程步骤中的责任也没有得到明确考虑。

因此，我们从部署方面回顾软件运行时修补的最新文献，以了解现有的运行时修补技术和方法。基于分析，我们提出一个分类法（在第3节中讨论），它提供了运行时修补解决方案的全面视图。

针对补丁粒度（第4节）、补丁方法（第5节）和补丁责任（第6节）的视角，我们还确定了运行时补丁中的挑战和研究空白，并在第8节中强调了进一步改进这一领域的未来研究方向。
本研究的其余部分结构如下。第2节讨论了软件修补的一般情况，接着第3节进一步深入概述了运行时修补。第4节考虑了各种运行时补丁粒度。第5节介绍了现有运行时补丁部署策略、工作流程和功能的全面视图。第6节包含了有关补丁过程中涉及的各方及其相应角色和责任的详细讨论。第8节概述了解决已确定的开放挑战的进一步研究机会，第9节总结了本研究。

2 BACKGROUND

图1展示了一个通用的补丁管理流程。无论更改的程度如何，更新软件系统都可以在线或离线进行。如图1所示，补丁准备、提供补丁、应用补丁、测试补丁以及可能删除补丁（如果适用）是关键步骤。补丁准备的技术取决于原始源代码是否可用。源代码补丁本质上是独立的、逻辑上统一的代码编辑，用于改进或修复某些功能、漏洞或漏洞。现代代码版本控制系统通常跟踪这些编辑作为代码提交。完全访问应用程序源代码使得开发全面和灵活的更改成为可能。然而，基于源代码的修补程序的主要缺点是需要重新编译整个应用程序以包括所需的更改。根据软件包的大小，重新编译步骤本身可能需要相当长的时间。

Untitled

相比之下，缺乏源代码访问权限意味着必须直接修改二进制可执行文件。因此，基于二进制的补丁基本上包含需要在原始二进制可执行文件中更改的字节。与源代码修补相比，二进制修补通常需要更短的时间，因为不需要进行漫长的重新编译步骤。然而，在准备阶段，二进制修补面临一个额外的挑战。即，必须在原始二进制文件中定位要更改的字节的地址。虽然超出了本文的主要范围，但值得注意的是，在生产系统中发生的所有更改都需要进行回滚规划，这是至关重要的。通常假定当新行为与期望的更改不匹配时进行回滚。这种假设可能意味着某些停机时间是不可避免的。因此，在进行回滚时，仍然优先考虑保持运行。因此，从总体上看，回滚操作等同于运行时补丁。相反的方向（新代码返回旧代码）。在两个方向上都必须考虑相同的自洽性问题。关键区别在于，在应用补丁之前可以进行更长时间的准备工作，而不是可能的突然失败。通常，回滚过程高度依赖于应用的补丁类型，涉及的应用程序数据，预期的影响，时间限制和代码量。本次审查旨在仅关注补丁部署步骤、方法和解决方案。

2.1 Traditional Software Patching

传统或离线修补意味着停止运行的软件实例，可能转换现有数据并启动一个新实例[9、14]。如图1所示，软件修补的第一步是修补准备。准备好的补丁针对源或二进制级别，具体取决于源代码是否可用。面向源代码的补丁需要进行可能耗时的软件重新编译以生成新的（修补后的）可执行文件，而面向二进制的补丁则修改现有的软件可执行文件。源代码级别的修补允许程序员轻松修改软件的任意方面，例如替换任何函数、指令和数据流。另一方面，二进制补丁在其本质上有些受限，并且主要用于较小规模的修改（主要在安全上下文中）。二进制修补的主要复杂性在于任何代码长度变化都可能导致重要的内存指针失效。此外，在二进制级别的修补中，找到要修改的错误部分的确切位置可能会很复杂[15]。此外，旧的二进制文件仍然可以运行，进一步复杂化了修补过程。此外，由于新修补的二进制文件已准备好执行，运行它可能会因资源共享而导致冲突，因为旧的二进制文件使用相同的资源。

传统补丁的挑战：传统软件补丁方法的主要缺陷是旧软件停止并且新软件未完全启动时会出现的服务中断[1，14]。例如，当补丁软件系统停止时，远程或本地用户会话、网络连接和数据处理会中断或暂停。在交互式用户会话中，短暂的中断可能是可以接受的（尽管不方便），例如网页浏览或文字处理。交互式软件通常被设计成自动保存和恢复用户会话，以在某种程度上减轻这种不便。试图在重新启动之间恢复状态的Web浏览器就是这种缓解的很好的例子。相比之下，对于高度关键的系统，在服务中断可能导致重大经济损失或完全不可接受的情况下，经历服务中断是不可取的。例如，对于生命支持软件和空中交通管制，禁止关闭系统或不被视为选项[14]。因此，系统管理员可能选择延迟补丁部署，以避免可能导致服务中断和应用程序状态丢失的系统重新启动。例如，更新用于高度交互活动（如在线游戏或视频流）的服务器操作系统通常需要安排服务器停机时间。在此期间，玩家必须停止游戏，等待服务器更新和重新启动，然后登录服务器，并可能从头开始游戏，这对玩家来说很麻烦。不幸的是，保持一个容易受攻击的系统未修补一段时间会增加被攻击的风险。为了克服传统修补的这些挑战，运行时修补已经出现并获得了广泛的认可。运行时修补的详细信息和相关优点将在第3节中讨论。

2.2 Existing reviews

近年来进行了几项与软件补丁和更新相关的评估[16-22]。Ahmed等人[17]对运行时软件更新解决方案进行了全面的系统映射研究。在分析大量论文时，我们遇到了一些不太结构化的方法分类。例如，最常引用的更新方法包括“Java VM”和“多版本”，它们不一定是互斥的。此外，尽管该研究提供了使用方法的统计数据和概述，但缺乏有关特定方法的好处和挑战以及技术、工具和算法采用之间的相关性的详细信息。 Seifzadeh等人[16]提出了一种更为结构化的运行时软件更新解决方案分类。该研究提供了一套全面的、高层次的运行时更新评估指标，例如范围、更新时间和类型安全。 Miedes等人[18]没有专注于现有实现，而是概述了一般运行时软件更新中使用的概念和技术。此外，还确定和讨论了一组目标和要求，例如服务连续性和普遍性。然而，该研究未提供这些方法的连贯分类或分类，导致一些分类不匹配。例如，尽管在目标方面是正交的，但Java导向的方法和可回滚性与技术挑战并列讨论。此外，一些评论关注特定的技术领域和使用场景。例如，Lopez等人[19]已调查了现有的功能和系统调用挂钩方法。虽然功能挂钩可用于多种目的（包括恶意），但应用挂钩技术可以显着提高功能级补丁的效果。此次调查的主要优点是综合考虑了主要操作系统下的功能和系统调用挂钩。然而，此次评论的范围仅限于功能粒度，未考虑其他补丁级别。 Gregersen等人[21]比较了三种现有的Java应用程序运行时修补实现。除了评估实现的性能外，还分析了低级修补能力。评论的范围仅限于Java特定功能，例如考虑了类修改。最后，Mugarza等人[22]关注了工业物联网领域的运行时软件更新。具体而言，通过核控制系统案例研究评估了安全系统的要求。与现有评论不同，Ilvonen等人[20]采取了一种有趣的视角，通过分析支持运行时或动态软件更新（DSU）在软件工程教育上下文中的情况。特别地，分析了现有的软件工程课程，以确定DSU概念的采用和覆盖范围。该研究的主要发现是，在教育中缺乏对DSU的整体方法，只有某些个体方面得到了关注。

根据审查研究，得出了几点观察结果。首先，在运行时修补领域，甚至在术语层面仍然缺乏共同理解。其次，迄今为止还没有清晰的分类法来协调现有的运行时修补方法。第三，缺乏通用性阻碍了现有的运行时软件修补方法和工具的更广泛采用。第四，评估指标因所需运行时修补领域而异，从通用时间开销到特定语言的类修改。

我们的调查范围：我们的调查重点关注运行时修补方法的多个方面，例如修补规模、通用策略和责任。我们提供了详细的分类法，并伴随着现有解决方案的相应分析。主要关注点在于修补管理生命周期中的应用修补阶段（如图1所示）。与现有调查不同的是，它们通常是狭窄的，主要强调用于修补的方法和工具，我们试图概括不同修补粒度级别固有的问题和方法。值得注意的是，我们的调查不比较不同技术或解决方案的性能，因为观察到的实验设置和执行环境差异巨大。同样，由于评估技术的高度多样性，不同实现侧重于不同的度量标准（例如停机时间、开销和长期修补连续性），因此不同的评估技术不能直接进行比较。自然而然地，旨在实现零停机时间的系统在其评估程序中甚至不会考虑这种度量标准。此外，我们指出现有先进解决方案的共同挑战，并提出一组未来发展方向。

3 RUNTIME PATCHING

运行时软件补丁旨在更新给定软件系统，同时保留运行进程和会话。如果不可避免地需要停机，运行时补丁方法侧重于最小化中断时间。周等人[3]将运行时补丁定义为“一种动态更新软件的方法，有效降低了软件升级常常伴随的停机时间和不便”。与传统的补丁方法相比，运行时补丁主要是二进制导向的，因为程序的运行二进制实例是在内存中修改的。代码的二进制表示需要在运行时用新的（即修补的）版本替换[3,23]。除了修补二进制的内存版本外，还必须相应地修补磁盘副本，以便在任何将来的重启中修补的行为保持持久。

运行时补丁必须注意需要转换为与新代码兼容的当前状态[24-26]，其中包括内存中的对象、数据结构和外部操作系统资源。一组现有的方法涉及各种运行状态转换的方面，例如更新点和状态转换器[7,8,27]。在这些方法中，补丁由新代码、安全更新点和必要的状态转换器组成。更新点本质上是适用于应用运行时补丁的时间窗口。特定于数据的状态转换器可以将当前程序状态转换为新版本。具体而言，运行时补丁系统会不断监视程序执行。当程序达到适当的更新点时，系统会加载修补代码，并开始根据指定的状态转换器进行程序状态转换。一旦转换完成，程序执行将继续进行，新版本将处于活动状态[24]。

在严重情况下，通常是对于大型和复杂系统，状态转换可能需要相当长的时间，引起明显的服务中断。例如，将现有虚拟机（VM）转换为与新的超级监视器版本兼容可能涉及到转换虚拟磁盘格式。考虑到现代磁盘的多个GB大小，这个操作可能需要相当长的时间。此外，在转换过程中不停止VM可能会导致磁盘内容在新磁盘映像最终确定之前发生变化。在这种情况下，运行时补丁可以选择分步执行转换，并仅在最后一个数据部分转换期间停止VM。

Untitled

我们注意到，在考虑需要修补什么时，调查研究所涉及的问题和提出的方法是不同的。因此，我们通过将相关的运行时修补研究按照目标修补的细粒度分组，提取出七个粒度级别。需要注意的是，仅有少数论文被归类为多个子类别的情况，即某些研究提出的方法可以在多个细粒度级别上进行修补。

第二和第三类别侧重于“如何”方面的修补以及采用的一般技术（修补策略）和给定修补系统实现的技术能力（在第5节中讨论）。我们确定了两种主要策略：状态转换和共存与衰减。在某些情况下，当修补所带来的变化不大时，直接进行状态转换是可能的。例如，添加一个对象属性或方法以反映新的（修补后的）功能可能很简单。相反，删除或修改现有函数可能会导致依赖先前行为的其他代码片段发生问题。因此，共存和衰减方法旨在根据会话或事务将旧数据对象和新数据对象分开，如果可能的话。换句话说，在使用中的旧（未修补的）对象不会被修改，而新的代码修补将针对更新的对象。稍后，在预先存在的会话/事务完成时，旧对象将被处理掉。实现能力直接反映了给定解决方案的实际适用性。例如，某些系统可能能够自动安全地检测更新时间窗口，而其他缺乏这种能力的系统必须依靠开发人员的手动协助。同样，能力较弱的系统可能需要额外的外部帮助来管理内存，以将修补后的代码加载或适应到RAM中。

在第四个类别中，我们已经确定了涉及的实体及其职责，这些职责是由修补系统考虑的。具体来说，我们关注的是“谁”负责应用补丁。现有的研究有三种常见的职责目标观点。首先，供应商支持的修补系统意味着原始软件系统的开发人员负责修补过程。其次，软件系统的最终用户需要对正在运行的系统进行修补。最后，独立的第三方修补程序尝试提供设施，以将通用补丁应用于现有的通用软件（在某些限制内）。这些情况在修补程序可用的先前知识量上存在差异。最重要的是，开发人员自然会访问原始软件源代码，而最终用户则不会。同样，原始开发人员会拥有更深刻的应用内部和逻辑知识。研究可以以其他方式进行分类；然而，我们的主要关注点是确定补丁应用的级别以及应用补丁的采用或建议方法。这有助于我们确定从业者忽视的运行时修补方法的问题，并确定未来潜在的有益方向。

4 RUNTIME PATCHING GRANULARITIES

本节介绍了运行时补丁中旨在描述要应用的补丁的规模和边界的预期补丁粒度。补丁粒度定义了一个责任边界，在此边界内通常不需要或执行状态变换。我们确定的研究被分类为七个组：指令级别、函数级别、进程级别、容器级别、虚拟机级别、超级监视器级别和内核级别。图3提供了在不同粒度下涉及到的对象或元素的概述。虽然大多数简单的补丁是针对在RAM中更改单个机器指令，但是复杂的补丁则是针对替换易受攻击的VM为固定VM。例如，图3显示，补丁指令需要获取内存指针，而补丁主机操作系统则需要修改物理硬件状态。将研究按补丁粒度分类可以洞察到应用补丁时需要修改的对象和元素。它进一步

Untitled

帮助理解补丁的影响（即更改/补丁后果的范围）。例如，更改较低层中的对象，例如物理硬件状态，会影响较高层对象，例如文件系统和操作系统对象。补丁准备和部署过程高度依赖于补丁粒度。例如，替换几个CPU指令仅涉及将相应的代码编译成目标CPU架构，而更新VM可能需要重建整个VM镜像。与每个粒度相关的技术问题在下面讨论。除非对整体功能行为产生重大影响，否则修补单个指令只需要考虑指令抽象级别。同样，用修补过的变量替换函数需要关注函数抽象级别，除非整个过程行为的变化在外部可观察。相比之下，转换到新内核需要处理正在使用旧内核资源的所有进程。选择适当的补丁粒度实质上是在内部状态和外部状态之间进行权衡。如图3所示，集合边界以外的连接点（例如网络套接字、外部函数调用和硬件）可能需要调整以匹配补丁代码。

4.1 Instruction-level Patching

指令级修补需要修补解决方案将更改的指令写入适当的内存位置。它旨在替换机器级CPU命令或RAM中的单个字节[2、15、31]。我们已经确定了一组已执行指令级修补的研究[2、7-9、15、31]。根据给定软件的源代码可用性，指令级修补的修补准备略有不同。在两种情况下，修补准备输出是要写入某个内存地址的字节序列(可能是动态计算的)。指令级修补比函数级修补更轻量级和更快速[9]。表1总结了提出指令导向运行时修补方法的研究，并确定了每个研究的目标以及与修补相关的任务，例如修补生成、部署、验证和恢复。通过目标，我们考虑研究的重点——例如，解决软件更新、修复错误、漏洞或修补特定攻击(如缓冲区溢出)的解决方案。表1还显示了修补任务是否完全自动化，需要人类手动输入来触发自动化任务(即半自动化)，还是完全依赖于人类。在大多数指令级修补解决方案中，修补部署后会自动进行修补生成[2、7、15、31]。我们进一步确定了修补的范围。由于技术和语言的变化，修补解决方案不是通用的；因此，特定研究的范围显示了所提出的方法是针对Linux、特定语言(如C)还是云系统。从表1中，我们可以看到大多数指令级修补方法都是自动化的，并跨越多个系统和应用领域。

Untitled

4.2 Function-level Patching

功能级补丁相对于指令级补丁更为粗略，因为它的目标是修补整个函数[4，34]。例如，它用一个修补过的函数替换有错误的函数以消除漏洞。一系列研究已经提出了进行功能级补丁[4，9，24，25，33-37]。进行功能级补丁需要考虑跨函数依赖关系。此外，长期存在的函数提出了进一步的挑战，因为必须确定合适的修补时间。与指令级补丁相比，定位修补目标地址的步骤并没有太大的区别。表2总结了与功能级补丁相关的研究。它显示了大多数功能级补丁研究，在修补部署之前执行修补生成。与指令级修补类似，这些研究的范围涵盖不同的领域、操作系统和应用程序。

一些运行时的功能级修补方法是为安全补丁而设计的[4，34，35，40]。例如，段安等人[35]提出了OSSPatcher，自动识别易受攻击的函数，生成二进制补丁并在运行时执行补丁注入。同样，李等人[34]提出了一个Appwrapper工具包，可以在每个方法（即函数）的基础上注入额外的安全代码到不安全的应用程序中，从而实现使用动态策略提高整体应用程序安全性。还可以通过将整个易受攻击的函数链接到内核中的新函数或替换代码来执行功能级修补。这种方法被认为对于被多个用户高度利用的大型服务器环境非常有用[4]。还有研究通过代码传输和函数的二进制重写来修补二进制程序的漏洞[40]。表2显示，大多数功能级修补是自动执行的，不需要用户干预。

Untitled

7 DISCUSSION

高性能和内存开销主要定义了运行时补丁的可行性，而不是传统的离线补丁。这些开销是由于现代复杂软件固有的执行状态的规模和确定安全更新点的困难所导致的。在医疗、军事或救援行动等关键任务领域，维持不间断的服务运营至关重要。资源丰富的高度关键的系统可以容忍运行时补丁系统常见的高性能或内存开销。然而，资源受限的系统如嵌入式物联网设备可能需要更高效的补丁解决方案，具有较低的性能或内存开销。我们对审查的研究的分析提示，供应商提供的补丁具有降低相关开销的更大潜力。对软件内部的深入了解以及软件的协作性质，简化了许多修补步骤。协作性质可以指请求控制的代码执行暂停，而不是突然的代码中断或漫长的等待静止状态。类似地，现有的旧代码可以协作提供正在使用的资源列表，而不需要复杂的手动资源跟踪。

根据我们提出的分类法，我们还得出结论，运行时补丁在开源生态系统中占主导地位，大多数补丁框架设计用于独立第三方使用，而不是软件供应商和消费者直接使用（如表6所示）。这可能解释了软件供应商没有足够关注运行时补丁功能。中间人角色似乎正在形成，专注于服务连续性。云基础设施是一个典型的例子，其中服务连续性不是软件供应商向终端用户提供的单独解决方案，而是由云服务提供商集成到云提供的服务中。访问源代码显著简化了应用程序内部的理解，使得可以开发适用于给定应用程序的高效运行时补丁解决方案。不将补丁解决方案限制在特定的供应商或最终用户也有助于补丁系统的普及度，因为它具有更广泛的适用性。

我们观察到一种常见的商业化趋势，即运行时修补解决方案通常不通过对修补系统本身进行货币化，而是将实际的修补作为付费订阅的一部分提供。例如，现有的商业解决方案，如TuxCare的KernelCare9、Oracle的Ksplice10和Red Hat的kpatch11，提供可以在运行时应用的修补程序。客户基本上支付适应和支持常规源级更改的运行时修补格式。请注意，某些类型的更改，例如语义结构修改或特定系统函数替换，可能会被某些修补解决方案明确不支持12,13。
.
我们进一步观察到，尽管这些专注于Linux内核补丁的商业解决方案取得了成功，但实际上内部使用的粒度不一定是内核级别，而可以在指令或函数级别上实现（表1-4）。值得注意的是，我们将Ksplice归类为函数级别的粒度。因此，根据补丁设计选择，可能需要实现不同的功能，如表5所示。例如，Ksplice选择不实现执行代码路径分派功能，同时支持我们的分类法所识别的其他三种补丁实施能力。

闭源商业运行时修补解决方案主要由相应的软件供应商开发、控制和管理。这是因为只有供应商才能访问软件源代码，这显着简化了补丁的开发和准备工作。因此，这种供应商策划的修补解决方案与软件紧密集成，不会单独提供给更广泛的受众。例如，微软采用了一种运行时修补解决方案，以最小化 Azure SQL 数据库引擎服务在补丁期间的中断14。根据他们的统计数据，超过80%的 SQL 错误可以使用这个修补系统得到纠正。根据我们的分类法，这种方法是一种功能级共存和衰退解决方案。尽管与特定的软件应用程序密切相关，由于补丁加载和函数重定向步骤的普及，类似的编译器辅助方法也可以用于其他基于 Visual C 的应用程序。我们发现的另一个商业解决方案，即 MuleSoft CloudHub 平台15，主要关注维护持续的云服务。由于封闭性，所提供的修补解决方案说明在实现细节上很少；然而，根据我们的分类法，它属于过程级共存和衰退解决方案。

请注意，虽然Python或JavaScript等某些动态编程语言提供了各种动态代码加载机制，但它们并不直接映射到实际的补丁内容。开发人员仍必须准备代码，通过编写将加载并应用的代码片段来进行必要的状态转换。尽管如此，动态代码处理的进一步发展是实现高效运行时修补系统的有希望的道路。

8 运行时修补的开放挑战和未来研究方向

根据进行的回顾，可以提出一些关于现有知识和努力中存在的差距的观察。简而言之，我们注意到，尽管进行了大量的研究和开发工作，但运行时补丁仍未得到充分利用。例如，最近一个有趣的Log4J漏洞被提议通过利用漏洞本身来修补。此外，尽管各个软件应用程序使用了各种运行时修补解决方案，但缺乏通用解决方案表明，在这个领域有重要的研究潜力，特别是开发编译器和操作系统内核增强方法。我们确定了许多未解决的问题和潜在的未来方向，这些问题和方向在图8中显示，并在下面的小节中讨论。首先，大多数现有解决方案的适用范围狭窄，且适用性严重受限。例如，运行时修补解决方案可能采用特定的语言或执行平台或操作系统特性，限制了这种解决方案的实用性。或者，只支持特定类型的更改（例如添加类方法），这对于非平凡的修改提出了挑战。

Untitled

其次，运行时补丁缺乏系统化方法的原因可能是当前实践中补丁开发的临时性质所导致。与已经成熟的众多开发实践相比，传统的软件开发已经被充分建立。补丁开发看起来不那么有条理。这是因为由于相关的安全风险，补丁通常是在紧迫的时间压力下开发的。高调的漏洞可能会导致巨额的经济损失，从而促使尽快部署补丁。这留给开发人员很少或没有时间系统地处理任务，导致补丁很快被补丁（有时超过一次）跟随，以修复最初的补丁被发现有漏洞的情况17,18。
.
最后，与传统的源代码级别修补相比，运行时修补能力往往被视为事后补救。
运行时补丁甚至可能不是独立开发的，而是从开发人员提供的源代码更改自动生成的。
这导致合作修补解决方案短缺，无法通过现有代码库提供各种程度的协助来简化进一步修补。
开发合作更新子系统需要在设计和开发阶段进行额外的努力。因此，在实践中并不常用。
此外，预见所有可能的修补和资源移交场景可能是不可行的，从而使这样的实现在长期内不够灵活。

8.1 Behaviour Change Compatibility

为了确保用户体验的连续性，必须维护机上活动与更新代码之间的兼容性。引入显著外部可观测变化的修补程序可能会导致与外部观察者的预期不兼容。因此，运行时修补系统的任务之一是实现代码和数据的兼容性，或者至少在补丁部署之前检测潜在的不兼容性。处理原始代码和补丁代码之间的潜在不兼容性需要确定不兼容性的范围（即补丁效果的可观测范围）和类型（即哪些方面变得不兼容）。例如，如果检测到某些不兼容性，补丁应用可能会被完全停止或推迟。检测最具破坏性的补丁可以帮助减少相关停机时间和服务中断。考虑到行为变化兼容性的上述问题，我们进一步讨论未来的研究方向，这些方向可能有助于解决原始代码和补丁代码之间不同方面的这些问题。

8.1.1 外部依赖跟踪。确定潜在的不兼容性在哪里需要跟踪代码的各个外部依赖项，这些依赖项也需要更新。例如，如果一个函数级别的补丁修改了函数接受的参数，那么调用该函数的所有外部代码片段都需要相应地进行更新。此外，需要递归分析依赖于调用修补函数的代码的进一步代码片段，以必要的方式传播更改。类似地，修补网络服务应用程序可能需要更新远程客户端软件以保留网络级服务兼容性。这个过程类似于常用于跟踪不受信任的用户输入流的递归污染跟踪，以识别和纠正不安全的输入使用[60]。一般来说，旨在安全的补丁试图最小化大幅改变代码行为。然而，可以认为，对于紧密集成的软件，即使是微小的补丁（函数或指令级别），也可能导致严重的副作用。因此，在运行时修补之前，了解补丁影响将可见的地方是关键的初步步骤。因此，研究和开发量化补丁影响评估技术将有助于检测潜在的外部不兼容性。还可以使用进一步的补丁影响评估技术来评估给定补丁的潜在破坏性。这种复杂度度量将使得可以正式验证给定补丁的影响。因此，可以立即应用不影响最终用户的简单补丁，而应用复杂和破坏性补丁则需要计划停机时间。准确地说，将估计外部可观察的软件行为变化，以确定给定补丁的影响。鉴于软件隔离（通过容器化和虚拟化）的趋势增加，需要特别注意可观察到的网络相关补丁副作用，即使在远程网络节点上也是如此。

8.1.2 代码和数据语义不一致性检测。当开发人员创建新的代码片段时，可能会无意中引入某些不一致性。简单的不一致性，如数据类型不匹配，可以通过维护类型安全性的方法自动检测。现有的解决方案通常试图通过跟踪变量数据类型的更改来实现类型安全。相反，语义差异（例如相同类型的变量的含义发生了变化）可能无法仅通过查看更改的代码片段来发现。例如，将整数变量更改为字符串变量可以被检测并相应地纠正[41]。然而，考虑一个不改变变量类型（即整数仍然是整数）但以不同的方式解释变量值的补丁（例如把米转成英尺）。通常，测量单位处理容易出现这种错误，同一距离/角度/重量变量可以用不同的方式解释（例如米与英尺，度与弧度，磅与千克等）。此外，执行从一种测量单位到另一种测量单位的转换的补丁可能会引入更多的错误。

将系统从一个转换到另一个可能不会导致类型不匹配错误（即违反类型安全），但仍可能在执行链的下游引起问题。检测这种语义变化无疑更加复杂，因为必须分析所有依赖于修补程序范围之外的变量的相关代码路径。不幸的是，迄今为止还没有提出可行的解决方案来检测语义不一致。也许类似于 𝜇DSU [61] 的元语言可以被调整以允许概述语义应用层。

8.2 Patch Deployment Overheads

除了技术实现问题之外，必须解决运行时修补的开销问题。这些开销主要集中在资源（例如RAM）和时间领域。基于共存的解决方案意味着必须同时在内存中存在多个代码或数据副本。这种共存对于较小的补丁可能不是问题；然而，在较长时间内应用多个补丁可能最终会带来挑战。同样，受资源限制的物联网设备也可能由于缺乏硬件资源而使一些解决方案不可行。例如，一些基于哈佛架构的微芯片可能不允许直接修改代码，导致需要重新刷新主存内容并重新启动执行。请注意，即使在这种受限制的设备中，某些扩展也已实施以帮助自修改，这对于修补目的是有用的19。必须预测架构、设备和资源限制的开销，以确定给定系统实时要求的修补适用性。我们在下面确定并讨论相关的定量度量研究方向。

8.3 Socio-technical Challenges

除了与运行时修补相关的纯技术问题外，几个社会技术方面也可能带来额外的复杂性。例如，由于内部政策或立法的实施而导致的延迟可能会显著减缓修补程序。组织可以考虑在设计阶段纳入运行时修补的软件开发实践。然而，根据改进的开发实践重写大型遗留软件包所需的货币和时间成本可能会使软件开发人员望而却步。此外，在某些情况下，供应链参与者（例如移动服务提供商或硬件供应商）可能会为了修补验证或安全分发而引入额外的复杂性。我们确定了一些潜在有益的研究方向，以解决阻碍运行时修补更广泛采用的社会技术挑战。

9 CONCLUSION

运行时修补技术和方法需要在安全和关键任务系统采用新兴技术后进行彻底的转型。在运行时应用补丁的关键步骤是最小化开销和停机时间。我们提出了一个分类法，突出了需要考虑的四个关键方面，以进行运行时补丁部署。我们识别和分析了七个补丁粒度级别，以及两种常规的补丁策略（状态转换和共存和衰减）和三个负责实体（供应商、消费者和第三方）。我们进一步定义了一个高层次的工作流程（图5），以支持四个关键实现能力，即（i）内存管理，（ii）资源转换，（iii）安全执行状态确定和（iv）执行路径分派。最后，本文回顾了挑战并提出了潜在的未来前景。我们认为，这个领域主要需要一种系统的方法来开发实用和方便的补丁解决方案，适用于各种基础设施、编程语言和执行环境。该领域还需要定义可量化的指标，以通过语义和依赖跟踪解决方案来确定补丁的影响。我们观察到许多需要供应商、最终用户和第三方考虑的开放机会和问题。

未来的研究方向包括通过实际的现场研究获得与修补相关的实际数据。通过分析这些数据，可以了解各个关键领域中现有修补挑战的统计数据。值得注意的研究问题应该集中在实践中常用的补丁程序、补丁粒度分布、应用的补丁复杂程度、补丁引起的系统停机时间和服务连续性，以及潜在的不兼容问题。总之，深入了解从业者和业务要求的问题和关注点对于弥合运行时修补研究与实际实现/部署之间的差距至关重要。

本文来自 eunomia-bpf 社区，我们正在探索 eBPF 和 WebAssembly 相互结合的工具链和运行时: https://github.com/eunomia-bpf/eunomia-bpf 社区关注于简化 eBPF 程序的编写、分发和动态加载流程，以及探索 eBPF 和 Wasm 相结合的工具链、运行时和运用场景等技术。

Posted 2023-03-23Updated 2023-11-2729 minutes read (About 4402 words)

论文阅读：将形式化方法应用于 Linux 内核中的 BPF 即时编译器

OSDI 论文：https://www.usenix.org/system/files/osdi20-nelson.pdf

yutube https://www.youtube.com/watch?v=2V3ts5-W_9g

摘要

本文描述了我们在 Linux 内核的关键组件之一，即 Berkeley Packet Filter（BPF）虚拟机的即时编译器（“JITs”）上应用形式化方法的经验。我们使用 Jitterbug 验证这些 JITs，Jitterbug 是第一个能够提供精确 JIT 正确性规范并能够排除现实世界中错误的框架，以及一种可扩展到实际实现的自动化证明策略。使用 Jitterbug，我们已经设计、实现和验证了一个新的 BPF JIT，用于 32 位 RISC-V，发现并修复了其他五个 JIT 中的 16 个先前未知的 bug，并开发了新的 JIT 优化；所有这些更改都已经被上游到 Linux 内核。结果表明，在仔细设计规范和证明策略的情况下，可以在一个大型未经验证的系统中构建一个验证组件。

据我们所知，Jitterbug是第一款提供了规范的工具，可以排除实际JIT实现中的错误，并提供了一种证明策略，可以将自动化验证扩展到一类编译器。通过规范和证明策略的精心设计，它展示了在正在积极开发的大型未经验证的系统（即Linux内核）中构建已验证组件（即BPF JIT）的可行性。本文描述了我们的设计决策以及背后的原理（§8）。

贡献

为了应对这些挑战，Jitterbug做出了以下贡献:
• 关于JIT正确性的精确逐步规范(§4)。该规范将BPF和目标架构都建模为抽象机器，并将JIT正确性表述为运行带有源BPF指令和JIT生成的目标指令的机器的行为等效性。该规范假定JIT一次只能翻译一个源指令。这个假设与实际的BPF JIT实现相匹配，避免了需要推理整个程序翻译的需要。
• 一种可扩展到实际BPF JIT的自动证明策略(§5)。Jitterbug在Serval [68]的基础上，使用符号计算 [10,89] 产生一个满足性查询，该查询编码了JIT实现、源BPF代码和JIT生成的目标机器代码的语义，然后使用SMT求解器 [21]进行查询。由于Serval是为静态已知代码的系统推理而设计的，因此无法用于验证由JIT的符号计算生成的符号指令(例如具有符号字段、在符号地址处)。Jitterbug通过一种符号计算策略来解决这个挑战，该策略可以推理这种符号代码。
• 一种基于C的领域特定语言(DSL)编写JIT的方法(§6)。Jitterbug DSL是一个基于C的浅嵌入式Rosette [88,89]的结构化子集，它扩展了Racket [29]来进行符号推理。也就是说，Jitterbug DSL将C的一个子集实现为一个Rosette库。我们使用DSL编写新的JIT，这简化了验证并支持JIT优化的合成 [59,82]。Jitterbug通过一个(未经验证的)提取机制自动翻译DSL中编写的JIT到C。我们通过手动将其C代码翻译为Rosette来验证现有的JIT。
•使用Jitterbug构建了一个面向RV32的BPF JIT，发现并修复了五个现有的BPF JIT中的bug，进行了代码审查，开发了优化，并为一个堆栈机器[65]移植了一个JIT，所有这些都具有较低的验证开销(§7)。其中一个bug已经导致了RISC-V指令集手册的澄清。我们报告了改进Jitterbug和将JIT代码上游到Linux内核的迭代过程。

Discussion and limitations

Jitterbug的JIT正确性（定义1），特别是使用跟踪的方式，受到CompCert [54]规范的启发。Jitterbug的规范有以下不同之处。首先，内核执行对源程序有更严格的要求（例如确定性，终止性和未定义行为的缺失），使我们能够证明更强的属性。其次，Jitterbug使用目标体系结构的细粒度模型来精确推理低级状态（例如程序计数器和堆栈指针），而CompCert使用更抽象的汇编语言语义[64: §5]，并依赖于单独的汇编器和链接器。第三，这种JIT的每个指令编译过程使我们能够开发逐步规范，方便自动验证。 Jitterbug相信假设的正确性（§4.2）。因此，它无法捕捉JIT上下文中的错误（例如可偏移构造）或目标程序的布局。我们手动检查Linux内核中现有的BPF JIT正确性错误（§3.2），并确定在82个错误中，规范可以捕获除偏移表构造之外的所有错误。这显示了规范的有效性。Jitterbug的规范允许“空”JIT实现，它在所有源程序上都失败；我们使用现有的测试套件（例如BPF selftests）来评估JIT的功能完整性。它专注于JIT，无法排除BPF检查器，代码映像的内存管理或内核使用JIT中的错误。它不模拟指令高速缓存或内存权限，依赖于内核正确刷新缓存并设置权限。它不提供任何针对微架构时序通道[32,48]的保证。

复现：jitterbug

https://github.com/uw-unsat/jitterbug

install requires:

sudo apt install racket
git clone --recursive https://github.com/uw-unsat/jitterbug
cd serval-bpf
raco pkg install --auto ./serval
sudo apt install z3

cannot find…

serval/serval/lib/solver.rkt:6:2: cannot open module file
module path: rosette/solver/smt/yices
path: /home/yunwei/.local/share/racket/8.6/pkgs/rosette/rosette/solver/smt/yices.rkt
system error: no such file or directory; rkt_err=3
location...:
serval/serval/lib/solver.rkt:6:2
context...:
/home/yunwei/.local/share/racket/8.6/pkgs/rosette/rosette/base/form/module.rkt:16:0
[repeats 1 more time]
/usr/share/racket/pkgs/compiler-lib/compiler/commands/test.rkt:395:27
/usr/share/racket/pkgs/compiler-lib/compiler/commands/test.rkt:397:0: call-with-summary
.../private/map.rkt:40:19: loop
/usr/share/racket/pkgs/compiler-lib/compiler/commands/test.rkt:1128:1: test
body of "/usr/share/racket/pkgs/compiler-lib/compiler/commands/test.rkt"
/usr/share/racket/collects/raco/raco.rkt:41:0
body of "/usr/share/racket/collects/raco/raco.rkt"
body of "/usr/share/racket/collects/raco/main.rkt"

remove all related to yices in jitterbug/serval/serval/lib/solver.rkt

system error

[ RUN      ] "VERIFY (BPF_JMP32 BPF_JNE BPF_X)"
--------------------
arm32-alu64-k tests > VERIFY (BPF_ALU64 BPF_OR BPF_K)
ERROR

error writing to stream port
  system error: Broken pipe; errno=3

see

https://github.com/emina/rosette/issues/88

ls /home/yunwei/.local/share/racket/8.6/pkgs/rosette/bin/
yunwei@yunwei-virtual-machine:~/jitterbug$ which z3
/usr/bin/z3
yunwei@yunwei-virtual-machine:~/jitterbug$ ln -s /usr/bin/z3 /home/yunwei/.local/share/racket/8.6/pkgs/rosette/bin/z3

用 z3 可能太慢，需要使用 boolector，同样需要放到对应的位置

注意不能 apt install，有版本要求

参考 https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html

需要从头构建 boolector

You may also wish to install the Boolector
SMT求解器。我们使用配置为使用CaDiCal SAT求解器的Boolector v3.2.1进行了测试。验证和合成将首先尝试使用它，然后再退回到Z3，这可能需要更长的时间（例如，合成可能慢了10倍以上）。

注意 Boolector 一般使用数十秒才能完成一条指令的验证，z3 可能要十分钟一条…

yunwei@yunwei-virtual-machine:~/jitterbug$ ln -s /usr/local/bin/boolector /home/yunwei/.local/share/racket/8.6/pkgs/rosette/bin/boolector

然后就可以运行啦

$ raco test racket/test/rv64/verify-alu32-x.rkt
raco test: (submod "racket/test/rv64/verify-alu32-x.rkt" test)
ENABLE_STACK_ADDR_SYMOPT=#f
ENABLE_JIT_SPLIT_REGS=#f
Using solver #<boolector>
riscv64-alu32-x tests
[ RUN      ] "VERIFY (BPF_ALU BPF_MOV BPF_X)"
[       OK ] "VERIFY (BPF_ALU BPF_MOV BPF_X)" (24578 ms)
[ RUN      ] "VERIFY (BPF_ALU BPF_ADD BPF_X)"
[       OK ] "VERIFY (BPF_ALU BPF_ADD BPF_X)" (32643 ms)
[ RUN      ] "VERIFY (BPF_ALU BPF_SUB BPF_X)"
[       OK ] "VERIFY (BPF_ALU BPF_SUB BPF_X)" (72785 ms)
[ RUN      ] "VERIFY (BPF_ALU BPF_AND BPF_X)"
[       OK ] "VERIFY (BPF_ALU BPF_AND BPF_X)" (32935 ms)
[ RUN      ] "VERIFY (BPF_ALU BPF_OR BPF_X)"
[       OK ] "VERIFY (BPF_ALU BPF_OR BPF_X)" (29574 ms)
[ RUN      ] "VERIFY (BPF_ALU BPF_XOR BPF_X)"

Finding bugs via verification

As an example, let’s inject a bug fixed in commit [1e692f09e091].

Specifically, remove the zero extension for BPF_ALU|BPF_ADD|BPF_X

in racket/rv64/bpf_jit_comp64.rkt:

[((BPF_ALU BPF_ADD BPF_X)
(BPF_ALU64 BPF_ADD BPF_X))
(emit (if is64 (rv_add rd rd rs) (rv_addw rd rd rs)) ctx)
(when (&& (! is64) (! (->prog->aux->verifier_zext ctx)))
(emit_zext_32 rd ctx))]

Now we have a buggy JIT implementation:

1
2
3

[((BPF_ALU BPF_ADD BPF_X)
(BPF_ALU64 BPF_ADD BPF_X))
(emit (if is64 (rv_add rd rd rs) (rv_addw rd rd rs)) ctx)]

Run the verification:

1	raco test racket/test/rv64/verify-alu32-x.rkt

Verification will fail with a counterexample:

[ RUN      ] "VERIFY (BPF_ALU BPF_ADD BPF_X)"
<unknown>: <unknown>: bpf-jit-specification: Final registers must match
--------------------
riscv64-alu32-x tests > VERIFY (BPF_ALU BPF_ADD BPF_X)
FAILURE
name:       check-unsat?
location:   [...]/bpf-common.rkt:218:4
params:
  '((model
   [x?$0 #f]
   [r0$0 (bv #x0000000080000000 64)]
   [r1$0 (bv #x0000000000000000 64)]
   [insn$0 (bv #x00800000 32)]
   [offsets$0 (fv (bitvector 32)~>(bitvector 32))]
   [target-pc-base$0 (bv #x0000000000000000 64)]
   [off$0 (bv #x8000 16)]))
--------------------

工具生成的反例给出了会触发错误的BPF寄存器值：它选择r0为0x0000000080000000，r1为0x0000000000000000。这证明了该错误，因为RISC-V指令对32位加法的结果进行符号扩展，而BPF指令执行零扩展。

Verification

验证工作的原理是证明BPF指令与JIT为该指令生成的RISC-V指令之间的等价性。

以一个具体的例子来说明，考虑验证BPF_ALU|BPF_ADD|BPF_X指令。验证从构建一个符号的BPF指令开始，其中目标寄存器和源寄存器字段可以采用任何合法值：

BPF_ALU32_REG(BPF_ADD, {{rd}}, {{rs}})

接下来，验证器在BPF指令上符号地运行JIT，产生了一组可能的符号RISC-V指令序列：

addw {{rv_reg(rd)}} {{rv_reg(rd)}} {{rv_reg(rs)}} slli {{rv_reg(rd)}} {{rv_reg(rd)}} 32 srli {{rv_reg(rd)}} {{rv_reg(rd)}} 32

这里，rv_reg表示与特定BPF寄存器相关联的RISC-V寄存器。

接下来，该工具证明了每个生成的RISC-V指令序列对于所有可能的寄存器rd和rs的选择以及所有RISC-V通用寄存器的所有初始值，具有与原始BPF指令等效的行为。为此，它利用了由Serval验证框架提供的自动验证器，具体如下。

验证器从符号BPF状态和符号RISC-V状态开始，分别称为bpf-state和riscv-state，假定两个初始状态匹配，例如，对于所有reg，riscv-state[rv_reg(reg)] == bpf-state[reg]。接下来，它在bpf-state上运行Serval BPF验证器，在riscv-state上运行每个生成的RISC-V指令序列上的RISC-V验证器。然后，它证明最终的BPF和RISC-V状态仍然匹配。

对于更复杂的指令，例如跳转和分支，需要额外的注意。有关详细信息，请参见lib/bpf-common.rkt:verify-jit-refinement中的JIT正确性定义。这种复杂性来自于必须证明生成的指令保持BPF程序计数器和RISC-V程序计数器之间的对应关系。

Synthesis for the RV32 JIT

为了帮助开发和优化RV32 JIT，我们使用Rosette的程序合成功能为BPF指令的一个子集综合合成每个指令的编译器。

综合过程以Serval的BPF和RISC-V解释器、BPF JIT正确性规范和程序草图作为输入，描述了要搜索的代码结构。综合然后在搜索空间中耗尽地搜索越来越大的候选序列，直到找到满足JIT正确性规范的序列。

您可以通过运行以下命令来尝试这个功能：

raco test racket/test/rv32/synthesize-alu64-x.rkt

它将产生类似于以下的输出：

`riscv32-alu64-x synthesis
Running test “SYNTHESIZE (BPF_ALU64 BPF_SUB BPF_X)”
Using solver #
Synthesizing for op ‘(BPF_ALU64 BPF_SUB BPF_X) with size 0
Synthesizing for op ‘(BPF_ALU64 BPF_SUB BPF_X) with size 1
Synthesizing for op ‘(BPF_ALU64 BPF_SUB BPF_X) with size 2
Synthesizing for op ‘(BPF_ALU64 BPF_SUB BPF_X) with size 3
Synthesizing for op ‘(BPF_ALU64 BPF_SUB BPF_X) with size 4

Solution found for ‘(BPF_ALU64 BPF_SUB BPF_X):
void emit_op(u8 rd, u8 rs, s32 imm, struct rv_jit_context *ctx) {
emit(rv_sub(RV_REG_T1, hi(rd), hi(rs)), ctx);
emit(rv_sltu(RV_REG_T0, lo(rd), lo(rs)), ctx);
emit(rv_sub(hi(rd), RV_REG_T1, RV_REG_T0), ctx);
emit(rv_sub(lo(rd), lo(rd), lo(rs)), ctx);
}

cpu time: 3513 real time: 141078 gc time: 324`

在这个例子中，综合算法能够找到一系列由四条RV32指令组成的序列，这些指令能够正确地模拟一个“BPF_ALU64 BPF_SUB BPF_X”指令的行为。这个解决方案被打印成一个C函数“emit_op”。你可以在“arch/riscv/net/bpf_jit_comp32.c”文件中的“emit_rv32_alu_r64”函数的“BPF_SUB”情况中看到它是如何被整合到最终的JIT中的。请注意，JIT中的指令可能与你的机器上求解器找到的解决方案不同。

你可以通过查看其他的“racket/test/rv32/synthesize-*.rkt”文件，并取消注释这些文件中其他指令的情况，来尝试合成其他指令。

并非所有最终JIT中的指令序列都是通过综合算法找到的。许多综合查询要么非常耗时，要么没有产生任何结果：特别是那些需要非常长的指令序列（例如64位移位），或者使用非线性算术（乘法、除法等）的指令。对于这些指令，我们手动编写实现，并使用本指南中描述的其他技术来验证其正确性。.

Generating the RV32 JIT

RV32 JIT分为两个部分：Racket实现在racket/rv32/bpf_jit_comp32.rkt中包含了为给定BPF指令生成RV32指令序列所需的代码，而racket/rv32/bpf_jit_comp32.c.tmpl是一个模板，包含了需要让JIT接口在C中编译并与内核的其余部分进行交互所需的粘合C代码。该模板包含了需要从相应的Racket源代码提取到C的空缺部分。

可以通过以下方式生成arch/riscv/net/bpf_jit_comp32.c和头文件arch/riscv/net/bpf_jit.h：

make gen

可以将这些文件复制到Linux内核源码树中进行构建和测试。

注意事项 / 限制

racket/test/目录下的测试用例显示了目前已验证的JIT指令。对于这些指令，它证明了对于所有可能的初始寄存器值、所有跳转偏移量、所有立即值等，JIT的正确性都是正确的。

验证一次只能证明单个BPF指令的JIT的正确性。目前尚未指定或验证JIT的几个属性：

对于riscv32而言，支持验证过程和收尾过程的有限支持。
对于呼叫/退出指令，支持有限:
- BPF_CALL，BPF_TAIL_CALL和BPF_EXIT 在riscv32和riscv64上支持；
- BPF_CALL和BPF_EXIT在arm32和arm64上支持。

验证做出了以下假设：

ctx->offset映射已正确构建。
BPF程序已通过内核的BPF验证器：例如，它假设没有除零或超出范围的位移。
BPF指令的数量小于16M，生成的RISC-V镜像小于128MB。这些边界可以增加，但会增加整体跳转的验证时间。
在验证的Racket JIT和C代码之间的翻译是可信的。任何翻译不匹配可能意味着C版本中存在的错误在经过验证的版本中不存在。

Posted 2023-02-14Updated 2023-11-272 hours read (About 13838 words)

综述阅读：安全实践中的形式化方法

A Survey of Practical Formal Methods for Security (acm.org)

在今天的世界中，关键基础设施通常由计算机系统控制。这引入了新的网络攻击风险，可能会破坏这些系统的安全性并破坏其功能。因此，有必要建立具有强大的网络攻击抵御保证的系统。实现这种保证的一种方法是使用形式化验证，它提供了系统符合所需网络安全属性的证明。本文回顾了在网络安全和安全关键系统方面使用形式化方法（FM）的情况。我们将FM分为三个主要类别：定理证明、模型检查和轻量级FM。为了比较FM的不同用途，我们定义了一组共同的术语。我们进一步根据应用FM的计算机系统类型来开发类别。介绍、讨论、比较和总结了每个类别中的解决方案。我们描述了历史亮点和发展，并从FM从业者和研究人员的角度介绍了FM在网络安全领域的最新研究现状。通过考虑所有类型的FM、几种类型的安全关键系统以及相应的分类结构，实现了全面的FM概述。因此，本文为安全关键系统的系统设计人员提供了FM和可用技术的综合概述，简化了选择正确工具的过程。本文总结了检讨的讨论，重点关注最佳实践、挑战、一般未来趋势和研究方向。

1 INTRODUCTION

数字服务目前正向社会各个方面扩展[207]。这反过来导致社会对支持这些服务所需的网络基础设施的依赖性。对网络基础设施的沉重依赖带来了新的挑战，形式是网络攻击和潜在的网络恐怖主义[142]，威胁行为者涵盖了从个人犯罪分子、网络犯罪分子和“黑客活动分子”到资源充沛的国家行为者[208]的整个范围。金融、工业或日常消费服务的干扰可能导致显著的财务和社会成本。随着数字化的进一步传播，潜在的攻击面只会变得更大，增加了保护数字服务的挑战[250, 260]。随着系统越来越大、越来越复杂，必须投入大量资源来保护这些系统免受已知网络攻击的攻击。通常，保护机制被纳入以关闭成功网络攻击后发现的漏洞，因此具有反应性质。这种方法将网络安全从系统内要解决的主要挑战降低到了一个事后的考虑[236]。

由于网络攻击的广泛性质，很难直接量化它们对社会的影响[101]，然而，它们往往涉及显著的财务成本以及可能的生活质量受损。一个例子是潜在的针对电力基础设施的网络攻击，包括电力市场，这可能导致发电机的损坏和机密数据的泄露[191]。另一个例子是针对制造设施的攻击，导致生产延迟或质量降低[47, 204]。这些例子表明，网络威胁应被视为对社会基础设施的物理威胁一样重要。

越早发现新系统中潜在的网络安全威胁，这些威胁的缓解成本就越低[257]。形式方法（FM）提供了在系统生命周期的所有阶段发现和缓解网络威胁的机会。使用FM为网络安全保证领域带来了数学严谨性。这是可能的，因为FM是使用基于模型的方法的技术，其中的模型被严格指定[261]，允许开发关于所研究的系统应该做什么的精确语句，而不会对如何做出任何约束[264]。这些模型代表所讨论系统的软件、硬件或二者的组合。使用FM的主要好处来自系统设计内部一致性的数学证明[115]。这种证明提供了强大的保证，因为它考虑了整个系统的行为，一旦证明为真，它就保持为真，而在传统的测试中，只能覆盖特定的场景。FM可以被视为提供数字社会网络安全保证的工具[262]。除了保证系统行为的正确性之外，采用全面的正式方法还可以减少实现错误的数量，这些错误是攻击的基本组成部分。

需要注意的是，存在各种各样的形式方法。我们考虑的主要类别是：

定理证明，基于计算机证明分析形式描述的重要属性。
模型检查，以详尽的方式检查系统的有限状态模型是否满足给定的规范。
轻量级形式方法，使用形式化技术对系统进行静态或动态分析（这个概念是在参考文献[132]中提出的，但我们从其描述中提取了模型检查并将其归为了另一类）。

有关形式方法在安全领域的技术基础的详细介绍，请参阅参考文献[32]。该章节重点介绍该领域的技术基础，而我们的调查则集中于特定的应用领域。在所有情况下，这些方法都被用来确定系统是否以正确的方式运行，许多方法都已经获得了重要的工具支持以自动化验证和验证过程[10]。在本次调查中，我们考虑所有方法及其在数字社会特定领域的应用。我们进一步将形式方法应用于系统行为的特定抽象级别，从应用级别到硬件级别。通过考虑形式验证在这些维度上的最新研究，我们提供了一个非详尽的概述，以特定学科的形式方法应用为例。本次调查的目的是允许从业者识别适用于其领域系统的经过验证的方法，从而希望增加形式方法在网络安全领域的应用。我们认为，在不同的形式方法应用领域进行类似的调查可能会成为增加应用的催化剂，因为已经确定，教育和经验以及找到形式方法的正面应用示例可能会导致专业人员将形式方法应用于他们的专业领域[104]。

1.1 Methodology

在应用形式化方法（FM）解决网络安全挑战的领域内，研究出版物的数量是相当可观的。因此，我们对于本次调查中所考虑的研究出版物做出了几项限制。首先是研究的新颖性，考虑到过去十年的情况，我们将出版日期限制在2012年之后。此外，所有的研究工作都需要在科学场合，如期刊、会议或研讨会上发表。下一个限制是专注于计算机工具支持的FM，即只有能够提供计算机分析并经常引导用户进行此分析的工具支持FM才被考虑。这一限制是为了更专注于FM的应用，将形式化安全分析的好处带给工业界。这与我们专注于应用形式化方法有关，在寻找研究出版物时，我们只考虑了使用工具支持FM来处理具体网络安全问题的研究出版物。因此，本次调查不专注于FM在安全领域的理论进展或仅简要提到FM使用的提议流程，如模型检查算法的理论方法、超属性规范等。此外，本次调查不涉及通常被称为可证明安全的安全方法。这是一种数学方法，用于分析加密机制或系统的安全性。该方法考虑攻击者模型下的系统，并将安全要求表达为一个对攻击者应该能够实现的限制。证明是通过建立攻击者需要解决一个已知的困难问题（例如二次残余问题[105]）才能破坏系统安全的事实来完成的。因此，系统的安全性降至基础难题的难度。该方法通常用于密码学领域而非安全系统，因此不在我们调查的范围内。我们指向参考文献[28]，提供了关于密码学中FM的报告。最后，我们将我们的搜索限制在明确考虑安全方面，而不是作为安全或正确性的副产品的研究。我们使用Google学术进行跨库搜索，重点关注研究论文，排除研究摘要或扩展摘要。

由于本调查为读者提供了研究的快速概述，我们进一步决定将不同的研究出版物按其关注的行业（领域）以及FM使用的抽象级别进行分类。通过这种方式，研究人员和潜在的工业用户可以快速找到他们感兴趣的领域。此外，我们根据发现的研究论文和现有文献的启示，将研究分类为基于网络安全问题分类。[208]。

1.2 History

本章介绍了过去40年中，在安全领域中使用形式化方法进行研究的重要案例历史。我们选择了四个案例研究，其中使用了形式化方法来保护系统的安全性：

(1) Needham-Schroeder公钥协议。Lowe使用了一个细化模型检查器来发现该协议的三角攻击。这是对先前由Burrows等人[52]证明正确的协议的新攻击。

(2) Mondex智能卡。这是第一个获得ITSEC E6级认证的商业产品。当时有很多讨论，关于是否可能实现这一点。

(3) Tokeneer ID站。人们对使用FM实现更高保证级别所需的严格性的可行性提出了类似的问题。Tokeneer解决了这个问题。

(4) seL4微内核。该系统被认为是世界上最可靠的微内核。显然，它证明了安全和使用形式化方法不会导致性能下降。

Needham-Schroeder公钥协议。Needham-Schroeder公钥协议是一种在网络设备之间进行通信的传输层协议[190]，为网络中的两个方提供相互认证。该协议在图1(a)中进行了可视化。它简单而广为人知，已成为测试安全协议验证技术的流行基准。我们在这里讨论它，因为它是一个重要的安全协议，但其中包含了一个重大错误。这个错误是通过形式化建模和分析发现的。

Lowe [165]表明，与其意图相反，该协议无法确保认证。特别是，他证明了入侵者可以在协议运行期间冒充代理A。冒充者欺骗另一个代理B，使其认为他们正在与A交谈。该协议使用公钥密码学。每个代理A都拥有一个公钥，任何其他代理都可以从服务器获取该公钥。A还拥有一个密钥，它是其公钥的逆。

任何代理人都可以使用A的公钥加密消息，但只有A可以解密它，确保保密性。该协议还使用随机数：为协议的单次运行造币的随机数字。 Lowe使用CSP [123]对协议进行编码，并通过CSP的模型检查器FDR [103]进行分析。Lowe没有直接指示FDR在协议中寻找漏洞-他只是对入侵者的能力进行了建模，但是模型检查器进行的详尽搜索发现了攻击，尽管如此。假设我（入侵者）是一个可以参与网络会话的网络用户。我还可以拦截消息并注入新消息，但无法在没有密钥的情况下解密消息。如果我发明随机数或已经理解消息的内容，则可以产生新消息。即使不理解内容，此入侵者也可以重播完整的加密消息[213]。这种方法通常称为Dolev-Yao模型[85]。攻击涉及协议的两次同时运行，如图1（b）所示。A与I建立有效会话。同时，我冒充A与B建立虚假会话。协议的错误运行可以解释如下：A向I发送一个带有随机数NA的消息，I使用I的秘密密钥解密该消息。 I向B中继消息，假装B正在通信。 B以A加密的方式回复NB，因此I将此加密的随机数中继给A。 A解密NB并向I确认它，I得知它。 I重新加密NB并将其返回给B，这使B相信A是另一方。攻击结束时，B错误地认为A是通信伙伴，只有A和B知道NA和NB。这表明协议是不安全的。协议分析师称这是中间人攻击。在这里，它已被自动发现。

Mondex。Mondex应用程序包括具有电子钱包（钱包）的智能卡，用于电子商务[235]。客户使用Mondex智能卡进行低价值、类似现金的交易，不需要第三方参与。英格兰银行（在这种情况下是金融监管机构）认为Mondex的要求是安全关键的：Mondex必须没有任何实现或设计漏洞，可以允许电子伪造。因此，开发人员将Mondex证明为当时最高标准的ITSEC E6级[129]，相当于通用标准评估保证级别7[57]。Mondex是第一个实现ITSEC E6（EAL7）的商业产品。参考文献[235]进一步描述了Mondex应用程序的开发，以及其抽象和具体模型。抽象模型描述了电子钱包的世界：原子交易交换价值，抽象模型表达了它们所需的安全性质。具体模型是钱包设计和价值交换的消息协议。设计团队使用Z符号[233, 263]指定了这两个模型。他们证明了具体模型在形式上是抽象模型的细化。这意味着具体模型遵守所有抽象安全要求。抽象模型及其安全性质通常比具体模型更容易理解。开发人员编写了手动证明，认为没有有效的自动化工具可以完成这样的大任务。相反，证明步骤使用fuzz2和Formaliser工具[97]进行类型检查。证明还得到了独立的外部评估人员的检查。

有四个主要的安全属性： • 系统及其用户不得创造价值。 • 系统必须记账所有价值。 • 钱包必须具有其预期交易所需的足够价值。 • 所有转移必须在真实的钱包之间进行。设计团队在证明发现漏洞后更改了辅助协议。该项目的详细说明在参考文献[265]中给出。 Mondex已被证明是一个可靠的安全系统，由其正式开发保证。

Tokeneer。Tokeneer系统是由美国国家安全局（NSA）[30]设计和开发的。它提供安全访问一个工作站的区域，并控制物理进入。访问控制需要生物识别检查和安全令牌。这些令牌描述了用户在访问该区域时的允许操作。开发人员需要确保安全性质。他们通过符合通用标准评估保障等级5 [57]来实现这一点。他们还需要展示他们可以以一种具有成本效益的方式来做到这一点。NSA邀请使用FM来开发Tokeneer系统的一个组件，并监控这个实验以测量执行开发所需的工作量和技能。 Praxis（一家英国公司）赢得了合同，并用Z [233, 263]编写了一个正式的规范，正式细化规范到一个SPARK程序。SPARK是带有附加工具集的Ada的子集[29]。他们证明了关键系统属性和运行时错误的缺失，使用传统方法开发额外的软件。这些额外的Ada程序提供了与外围设备的接口。该项目需要260人天，三人兼职，以及九个月的经过时间。它产生了约10K行SPARK代码，约有16.5K个合同。在实施阶段平均每天写作约200行代码，整个项目大约40行代码。另外还产生了3.5K行标准Ada代码，实施阶段平均每天约200行代码，整个项目约90行代码。系统测试耗时约占项目工作量的4％，远小于通常的测试。在Tokeneer中发现了两个缺陷。一个是通过形式分析发现的，另一个是通过代码检查发现的。测试团队发现了两个范围内的故障：用户手册中缺少的项目。 NSA设置的任务是符合通用标准评估保障等级5。Tokeneer开发实际上在几个方面超过了EAL5的要求：配置控制，故障管理和测试。尽管核心开发工作的主体是以EAL5为基础进行的，但涵盖规范，设计，实施和通信的开发领域是以EAL6和EAL7完成的。为什么？因为这样更便宜！

seL4微内核。第三代微内核seL4提供虚拟地址空间、线程和进程间通信的抽象。它提供明确的内存管理模型和授权能力。保证ARM版本的seL4微内核的二进制代码是正确的实现。seL4符合其抽象规范，不做其他事情。特别是，seL4 ARM二进制符合完整性和机密性的经典安全属性。 seL4微内核的C代码已经通过其抽象规范进行了正式证明。此证明在Isabelle/HOL中进行了机器检查。这假定启动代码、缓存管理、硬件和手写的汇编代码的正确性。开发人员声称seL4是唯一经过验证的通用操作系统（OS）内核。系统的操作模型形成一个抽象规范。Haskell程序原型化内核。这个原型提供了自动转换到Isabelle/HOL。Isabelle代码然后是内核的可执行的、设计级别的规范。这是手工编写的C代码，形成了高性能的C实现seL4。细化证明链接规范和C代码。开发者证明攻击者不能破坏内核，即使他们使用错误的编码、虚假的调用或缓冲区溢出攻击。

1.3 Definitions/background

在本文中，我们提供了一组通用术语和定义。这非常重要，因为形式验证和安全领域在很多年内独立发展，因此一些术语被过载并且具有稍微不同的含义，取决于它们在何种上下文中使用。例如，在安全领域（特别是密码学中），证书是指用于将实体绑定到加密密钥的文档。然而，在FM中，证书被用作系统或协议正确性的证明。

在本调查中，对于安全方面，我们使用身份验证一词来指识别和验证访问系统的用户（实体或个人）是否是用户声称的人。这与授权相反，后者是基于用户身份允许用户访问系统的过程。此外，我们经常发现安全协议旨在提供特定的属性，例如隔离，这是一种设计原则，其中进程被分离并被赋予对共享资源（例如共享内存）的特权访问（通常使用容器化或虚拟化等技术）。或者不可否认性，确保无法否认语句或消息的有效性，特别是其作者。我们还想指出匿名性和保密性之间的区别，匿名性指用户或进程的身份不得透露，而保密性指编码为数据块的内容不得透露。

在形式方法方面，可以说所考虑的系统通常包括一组协调的进程，这些进程是定义一组指令的程序实例，由一个或多个线程执行。我们认为进程是系统中的主动实体，而程序是被动实体。描述进程行为的形式框架包括CSP，CCS，ACP，π演算等。进程通常实现协议，即一组数据传输规则，并且可以在共享内存上进行同步或通过通道进行通信，通道是物理通信网络的抽象。由于使用了中间处理器缓存，共享内存实现变得越来越复杂，可能实现许多不同的一致性模型[6]。同样，可以对通道进行许多不同的假设，例如消息的FIFO排序；通道是否保证完整性、可用性和保密性；通道是否无误；是否可以区分消息类型等等。

一般来说，验证是针对规范的，规范是实体（例如硬件、系统、计算机程序、数据结构等）允许行为的抽象（形式或非形式）描述。正式验证通常是针对系统模型进行的，该模型提供了实体的精确正式描述，捕捉被建模实体的关键特性。必须确保模型描述的每个特征都是实体的实际特征。可能会开发相同实体的不同模型，这取决于所关心的属性；例如，计算机程序可以通过前/后状态之间的关系、状态轨迹、输入和输出之间的函数等进行建模。模型可能描述行为功能、协议等。在形式方法中，通常在多个抽象级别上开发模型，并精确定义这些级别之间的关系。安全性的形式方法还需要攻击者的模型，例如在通信系统环境中使用的 Dolev-Yao 模型。

在硬件验证中，术语“协同验证”用于证明系统软件在底层硬件设计的表示上正确执行。这使得软件与硬件集成，而不需要任何物理设备（例如芯片或板）可用。验证的目的是确保它符合其实现（规范）的要求，即实体的物理表现形式。在某些情况下，可以将实现称为模型，该模型提供有关实体的足够细节，以便可以轻松地获得相应的物理实体。

为了最终确定FM的定义，重温我们对FM的分类很重要。我们分类的第一类是定理证明，其中提供了系统正确性的证明，采用符号逻辑。本调查重点关注自动定理证明，其中利用证明助手生成证明。该方法利用一个逻辑系统，试图确定语句ϕ是否从一组语句Γ = {ψ1，…，ψn}中得出。我们考虑的第二类是模型检查，其中利用一个系统的有限状态模型系统地搜索此模型中包含的所有可能系统状态（即模型中的所有可能系统状态）以便检测有关系统的语句是否存在反例，例如在线性时间逻辑中表示为p的属性，表示属性p在无限多个状态中成立。与定理证明一样，我们重点关注自动模型检查。最后，我们定义了一类轻量级形式方法，其中放置了不提供详尽分析的方法。一个简单的例子可能是静态代码分析，其中分析代码时不运行以确定是否违反预定义的规则。另一个例子可能是VDM [38]，其中使用形式建模语言对系统进行建模，并将属性表示为合同，例如inv t == t.issueTime < t.expirationTime，表示通常必须在t到期之前发出t。为了执行检查，模型被动画化，仅设置特定场景（通常是被认为是关键的场景），但是，VDM也可以利用组合测试结合输入路径生成大量测试，从而显着增加测试覆盖率。

2 SURVEY

2.1 分类和概述

由于安全领域中的形式化方法应用于许多领域，我们根据领域和抽象级别进行分类，以提供广泛的安全领域FM的系统概述。我们选择的四个领域的标签如下：

金融（第2.2节）：聚合了在金融/货币领域应用FM的工作，例如支付系统、家庭银行、金融市场、加密货币等。例如移动银行应用程序，ATM基础设施，FIX股票交易协议，智能卡/硬件钱包等。

工业（第2.3节）：该标签聚集了处理应用于生产商品或服务、制造和工业控制的计算系统的工作。例如水处理管理面板，PLC控制网络，Modbus/TCP，电机控制器等。

消费者（第2.4节）：这个标签分类了关注终端用户/个人个人计算设备和应用程序（如命令行shell、家庭操作系统、VoIP协议和运动智能家电）的安全性的作品。

企业（第2.5节）：这是消费者类别的对应，用于分组关注提供计算服务以满足组织需求而不是个人的企业系统的安全性的作品。例如电子邮件服务，电子政务系统，sn2协议，数据服务器仓库等。

由于仅展示四个领域只会将FM在安全领域的研究按应用领域分开，我们进一步介绍了五个抽象级别，这些级别是进行形式化验证的级别：

应用：用于将FM应用于计算应用程序或计算目的的作品的级别。

系统：用于将FM应用于架构级别的作品，通常涵盖多个子系统。

协议：用于应用FM以断言属性或分析系统组件之间的通信协议的级别。

实现：这是一个横向类别，包括所有专注于直接在结果系统上应用/使用FM（例如运行时监控）而不是强调设计和规范的作品。

硬件：用于对在硬件开发过程中应用FM的作品进行分类。

这种分类使我们能够系统地审查最新的研究成果，并基于此提供概述。为了清晰地概述安全领域中的FM，我们进一步应用了第三个维度，定义所使用的FM类型，即模型检查、定理证明和轻量级FM。这提供了不同研究工作的数量概述，如图2所示。

此调查中的各个部分按照逻辑顺序组织，其中研究工作根据应用程序、系统、协议、实现或硬件类型进行分组。在此分组中，研究工作进一步按照逻辑分类组织成段落。例如，第一个段落可能会考虑与制造相关的工作，而下一个段落则会考虑与工业控制相关的工作。在这两种情况下，研究旨在工业领域，但具有不同的范围。调查中的每个部分都代表一个单独的领域，我们在不同抽象级别上提供了研究工作的系统总结。由于此调查试图对大量的研究工作进行分类，因此每个研究工作仅简要介绍，重点关注分析的问题和使用的FM技术。有关单个研究工作的更多详细信息，请参阅本调查基础的技术报告[149]。

消费者物联网系统，例如智能家居设备存在安全漏洞，并已经通过FM得到广泛验证。参考文献[153]的作者使用AVISPA中的模型检查工具和BAN逻辑来验证一个框架，确保智能家居环境中的匿名、身份验证和完整性。在参考文献[182]中，作者开发了IoTRiskAnalyzer工具，用于帮助工程师应用最适合的安全策略。这是通过使用马尔可夫决策过程[202]、将风险属性形式化为概率CTL公式，并使用PRISM模型检查器[156]进行验证实现的。汽车制造商也利用连接设备，特别是智能手机。例如，参考文献[53]的作者开发了基于智能手机的防盗装置，使用ProVerif针对Dolev-Yao攻击模型进行正式验证，以确保安全要求的强大保证。

2.5 Enterprise

企业和大型公司计算是大型国际企业的支柱。近年来，在企业计算中利用云解决方案的趋势仍然存在，同时仍然经常在本地数据中心运行。这些数据中心和云集群被用于众多企业任务，例如协作平台的虚拟化、公司管理和企业门户网站的托管。本节概述了利用FM解决企业计算安全挑战的情况，包括安全数据存储、虚拟化和软件定义网络安全、使用硬件令牌的强身份验证。由于企业是更大的实体，变化通常较慢，需要进行良好的管理。为此，FM已被用作企业云采用的助推器，因为已经提出了几种基于FM的解决方案，可以使企业从本地数据中心安全切换到联合云解决方案。与之前的章节类似，模型检查是企业计算中形式化安全分析中最常用的工具。定理证明也不落后，尤其是在分析企业服务器中的可信平台模块芯片方面。由于轻量级FM通常作为软件开发环境的插件提供，使它们易于访问，因此在实现层面上广泛使用。企业部分中涉及的网络安全主题如图6所示。

Application.

企业应用程序通常处理和存储对组织至关重要的数据。如今，这些数据通过软件定义网络（SDN）传输。参考文献[226]的作者创建了一个验证平台，用于利用SDN的应用程序，该平台包括一个建模语言，可以自动翻译并分派到PRISM、SPIN和Alloy模型检查器。任何反例都将显示在工具中。与SDN类似，面向服务的体系结构（SOAs）经常在企业应用程序中使用，增加了这些应用程序的互连性。在参考文献[20]中，作者提出了一个安全平台

利用正式的规范语言和几个模型检查器（CL-Atse和OFMC）对SOA进行评估。作者发现了Google Apps中SAML-SSO集成的问题。企业数据通常存储在大型关系数据库中。在这种情况下，参考文献[61]的作者提出了一种安全外包数据库到不受信任的服务器的方法，建立在可验证数据库[36]的概念上，并利用定理证明来证明他们的方法是安全的。虚拟化是云中经常使用的另一种技术。参考文献[222]的作者介绍了一种针对Xen hypervisor安全的正式分析方案，包括模型检查和静态分析，成功地重新发现了已知的漏洞。最后，我们想指出参考文献[72]中的工作，描述了一家领先的云提供商如何利用FM保障其服务的安全性，指出FM的好处对于他们的客户至关重要。

System.

现今，大型企业可以自行托管基础架构，充分利用云服务，或部分地将其基础架构与云服务结合，导致联合云系统[183]的出现。参考文献[270]的作者们提出了一种利用CPN和CPN工具[137]分析联合云行为的方法，并创建了几个模型用于安全分析。同样，参考文献[256]的作者们使用Z与Z/EVES定理证明器对数据交换系统进行了机密性和完整性属性的形式化分析，同时利用域理论[39]生成了测试。在参考文献[135]中，作者们提出了一种基于移动环境[55]和不干扰的带盒环境演算[51]的防火墙规则和云拓扑分析的形式化方法。由于云计算通常是利用共享资源构建的，因此参考文献[169]的作者们建立了一个离线框架，用于形式化分析网络隔离属性，确保共享资源之间的隔离。这是通过使用一阶逻辑和约束满足求解器Sugar [240]来完成的。同样，参考文献[173]的作者们提出了一个云复杂性管理（代理）系统[113]的安全框架，利用Z/EVES定理证明器在NIST [43]云参考架构中分析了几个云安全属性。

此外，在参考文献[232]中，作者们提出了一个代理解决方案，用于自动将云服务与客户进行配对，同时管理云复杂性。代理的一个重要部分是找到一个满足客户安全要求的服务，使用基于一阶关系逻辑[130]定义的KODKOD有限模型查找器[244]。此外，还有一些研究考虑了云系统内的虚拟化。例如，参考文献[117]的作者们提出了一种在虚拟化系统中分析安全性和信任的形式化框架，将硬件和软件模型结合在一起，用CSP#[238]表达，并分派给PAT模型检查器，发现了一个现实世界云系统中微妙的错误。同样，参考文献[42]的作者们提出了一个安全子系统，用于在与安全策略相关的虚拟化基础架构中进行变更分析，利用图形和图形转换分派给GROOVE模型检查器[102]。

协议。

企业计算正向云平台转型，需要安全通信协议，并受益于FM分析。Amazon云服务[13]使用s2n[14]，TLS协议的开源实现，利用FM证明其正确性。例如，在参考文献[64]中，作者们证明协议使用的基于哈希的消息认证码（HMAC）是不可区分于随机生成器的，使用Cryptol规范语言[89]描述HMAC，然后将其分派给Coq定理证明器，并通过软件分析工作台[100]将结果与实现相连接。在微软云中，参考文献[136]的作者开发了一种网络协议分析工具，利用Z3 SMT求解器来协助数据中心内的网络策略维护任务，为Azure云服务提供了重要的安全工具。由于云服务通常是远程访问的，参考文献[151]的作者利用Alloy分析器来查找SAML协议[125]中的漏洞。如今，云平台从小型IoT设备[185]收集数据，促使参考文献[141]的作者提出了一种轻量级双向认证协议，并使用OFMC和CL-AtSe验证其对多种攻击的抵抗能力。类似地，参考文献[212]的作者提出了一个移动设备认证方案，并使用ProVerif进行验证。IoT设备可以利用5G网络，参考文献[33]的作者使用Tamarin查找认证子协议问题，参考文献[8]的作者通过用CSP表达认证框架协议[269]和移动以太网协议[128]的方式进行分析，并将其分派给FDR模型检查器以评估相互认证属性。

实现。

企业计算通常由使用不同技术实现的许多应用程序组成。例如，参考文献[195]的作者创建了一个用于PHP插件的静态代码分析工具phpSafe，然后利用它发现了多个PHP插件中的580多个漏洞。类似地，参考文献[267]的作者创建了一个利用不变式分析[116]进行恶意行为检测的工具，指出在多个Web应用程序中逻辑漏洞的高效性。

虚拟化是企业计算的重要组成部分。为了实现虚拟化的安全性，参考文献[252]的作者创建了一个基于行为契约的安全验证虚拟化框架，并使用FRAMA-C[225]对行为契约进行静态分析。类似地，参考文献[251]的作者创建了一个虚拟化框架，用于在单个客户虚拟化程序中验证内存完整性，利用CBMC模型检查器[67]自动分析大部分代码库。

硬件。企业计算需要大量的云硬件基础设施和数据保密性、计算安全性等保障。客户通常将云提供商视为不受信任的实体，因为管理员本身可能构成威胁。

3 FUTURE OUTLOOK

此次调查概述了FM在多个领域中的安全应用情况。根据这些领域内的研究，可以预见在某些情况下FM的使用将加速，而在其他情况下，FM的使用将以较缓慢的速度增加。然而，一般来说，采用FM的趋势是增加的。在金融领域的情况中，FM的使用显然伴随着新的金融技术，如加密货币和智能合约。这种采用可以在专门针对智能合约领域的调查中看到[119]。金融领域中移动应用程序的使用也促使对通过使用FM可以提供高安全性保证的需求。最后，随着加密货币的兴起，金融领域内的硬件正在专门用于促进交易。预计在未来，这种硬件的安全性将继续得到形式化的审查，并且涵盖范围和复杂性将不断增加。

工业领域在网络安全领域面临着自己独特的一组挑战。随着自动化复杂性和数字技术在关键工业设施中的使用增加，预计FM将发挥至关重要的作用。这种趋势已经在2015年由[148]提出，他们调查了工业控制系统安全性和安全性的方法，包括非正式方法。到目前为止，该领域内的大多数工作都是反应性的，即现有系统和协议的分析。然而，在调查中，有几项工作显示了一种趋势，即在新的工业设施和协议的设计过程中早期利用FM。工业领域内另一个新兴趋势是将形式验证工具与软件开发流程集成，这主要表现在机器人应用和PLC代码方面。随着机器人应用和底层硬件的复杂性不断增加，预计FM在未来将发挥重要作用。

消费计算领域是一个快速发展的领域。消费者的趋势变化很快，然而，已经提出了相当多的工作来利用FM 恶意软件保护[37]，甚至创造了经过正式验证的互联网浏览器。此外，从计算机到智能手机的计算转移带来了新的安全挑战。在这个领域，已经将很多关注点放在了Android操作系统权限系统的分析上。这个领域显示出研究量的增加，并且只要移动操作系统被数百万用户使用，形式验证就会加速，可能导致流行的移动操作系统的完全形式安全验证。消费类硬件，如智能手机正在使用TPM，保护移动计算。此外，在这个领域，FM的使用正在增加，特别是为了确保安全TPM区域的属性。最后，企业计算领域揭示了几个有趣的趋势。其中之一是使用FM来针对虚拟化超级管理程序，分析现有虚拟环境的安全属性以及利用该知识构建完全形式验证的超级管理程序。另一个重要的趋势是主要云计算提供商对其产品的安全性进行形式验证的重大投资。为此，不仅应用了现有的工具，而且云提供商已经转向开发自己的FM工具。这两个趋势都预计不仅会继续，而且由于云计算和虚拟化的日益普及而加速。

安全威胁[217]。在这方面，[219]的作者创建了一个云隔离系统，将用户数据与管理员分开，并限制管理员对用户虚拟机的操作，利用硬件模块，作者命名为Trusted Cloud Module（TCM），为云管理员提供有限的接口，管理加密密钥，并为用户提供安全存储。该模块由现成的硬件组件构建，使用Scyther验证工具。同样，任何可信计算的基础是提供安全存储和计算环境的可信平台模块（TPM）协处理器。不幸的是，使用TPM的平台的安全性经常没有正式验证，导致漏洞[50]。为了缓解这一问题，[27]的作者提出了TRUSTFOUND，这是一个形式建模框架，用于利用Trusted CSP#，CSP#的扩展和LS2[77]进行模型检查，其中使用PAT模型检查器进行验证，并检测到六个隐含的假设和两个严重的逻辑缺陷。

有时，企业使用小型一次性密码（OTP）生成硬件来为用户提供强认证以访问云服务[45]。其中一种设备是Yubikey，一种USB OTP生成器。在[154]中，作者已正式分析了Yubikey OTP的安全性以及硬件安全模块（HSM）的安全性。在这个领域的另一个挑战是解决CPU侧信道攻击。其中一个攻击是时间信道攻击，在共享环境中，攻击者（可能是虚拟机）可以确定另一个虚拟机执行的算法。为了解决这个问题，[92]的作者提出了Timing Compartments，这是一种在硬件中实现的隔离方案，可隔离共享资源的各方之间的时间信息。该方案通过使用SecVerilog进行信息流分析进行了检查。

4 CONCLUSIONS

超过30年前，Burrows等人发表了他们关于安全协议分析的BAN逻辑的开创性工作[52]。他们的工作并不是完全正式的，被证明可以批准危险的协议。尽管如此，他们表明他们的逻辑在揭示各种微妙的安全缺陷和缺陷方面表现良好，特别是在认证协议中。他们着手回答五个问题：（1）这个协议是否有效？（2）它能够工作吗？（3）这个协议到底实现了什么？（4）这个协议是否比另一个协议需要更多的假设？（5）这个协议是否做了任何不必要的事情？

他们的重要论文启发了一代安全研究人员使用FM来设计和分析安全协议以及回答类似的问题。此外，在描述形式验证在软件工程中的好处时，Dijkstra曾经引用过著名的话：“测试只能证明漏洞存在，而不能证明漏洞不存在。” 50多年后，在计算机安全领域中，我们现在可能已经有足够的证据来声称“形式方法只能证明安全漏洞的存在，而不能证明不存在” [54]。也就是说，虽然FM提供了严格的工具和技术来证明安全漏洞的不存在，但这种严谨性是有条件的：只有在安全漏洞被记录和规定在一个正式的框架内时，才能进行证明。目前的局限性意味着，FM无法发现任何新的漏洞，因为我们可能并没有在寻找它们。

例如最近的Spectre和Meltdown攻击[145]。像许多漏洞一样，这两个攻击已被证明存在于使用推测执行的处理器范围内，并且缓解这些漏洞需要软件方面的干预。然而，尽管这些漏洞的普遍性，但攻击本身并没有通过形式验证发现，而是通过一系列关于微架构组件的训练和定时的实验。幸运的是，一旦发现了安全漏洞，即使是像Spectre和Meltdown这样复杂的攻击也可以得到正式的描述和隔离[59]。一旦这样做了，下一步就是一个形式的框架来推理这些问题，然后是更简化的工具来扩展验证到更大规模的系统。因此，对于在安全领域继续研究FM实际应用的重要性，同样重要的是通过研究该学科的理论方面来扩展我们在安全领域中FM的推理能力。如果没有这样做，就有可能出现一种新的安全漏洞，它超出了当今逻辑的范畴。例如，Spectre和Meltdown的变体可以通过子集闭合超属性[59]来捕获。因此，如果没有关于超属性[68]的现有作品和随后关于它们验证的作品[59、106、107]，FM的规范和使用来保护Spectre和Meltdown将会更加困难。

至于不同FM技术的利用，我们发现模型检查通常是分析更广泛系统的实践者的选择。从调查的作品中可以看出，一个趋势是，由于大量的工具支持、可以选择的建模语言的丰富性、能够进行详尽分析以及专门针对安全分析的模型检查器的存在[200]，模型检查通常被认为是一个好方法。我们可以确定，即使在模型检查会因问题规模而受到影响的问题上，作者也会将问题范围缩小，专门针对系统或应用程序的关键部分进行分析。在某些情况下，由于问题的规模过大或问题的适用性，FM实践者选择利用定理证明。虽然工具支持不及模型检查，学习曲线更陡峭，但定理证明提供了对会使模型检查器不堪重负的系统的详尽分析。然而，我们观察到，定理证明需要变得更加可访问，以增加其利用率。最后，轻量级FM的特殊类别提供了一个有趣的进入FM世界的入口。一方面，无法进行详尽分析可能被视为缺点，但另一方面，可以主张轻量级FM正在工程世界中变得普及。例如，静态代码分析器不仅在软件构建工具链中得到使用，而且经常直接集成到软件集成开发环境中[221]，成为世界各地大量软件开发人员的指尖工具。正如在第3节中思考的那样，这可能是将FM带入系统设计和开发前台的催化剂之一。

在本文中，我们展示了FM迄今对社会产生了什么影响，以及这种影响将来会增加。过去，安全曾经是工业在开发过程中不想投资的可选附加项。但是现在情况正在改变。例如，安全已成为必须的关键要素，行业不得不在开发过程中投资安全,Amazon Web Services的一个核心卖点是弹性计算云（见第2.4节）。FM已经成功地应用于金融、工业、消费和企业领域的安全分析中（见第2节）。

规范语言和相关工具

我们的调查涵盖了超过十年的FM在安全领域的应用。它揭示了正式规范语言及其工具、定理证明器、模型检查器和验证框架的丰富多样性。我们记录了超过40种不同的规范语言和超过40种不同的验证工具。其中包括以下内容：

Specification languages. AADL (Architecture Analysis & Design Language) [18, 70], ASF (Anonymous Secure Framework) [153], ASLan++ (AVANTSSAR Specification Language) [20], BAN logic [52, 228], Boogie [31], Boxed Ambients [135], CASM (ASM-based SL for compilers)[252], CCS (Calculus of Communicating Systems)[152], COVERT (compositional analysis of Android apps) [26], CSP (Communicating Sequential Systems) [120], CSP# (shared variables CSP) [237], CTL (Computation tree temporal logic) [229], Cloud Calculus [135], Cryptol [89], Dynamic State Machine [187], ERC20 token contracts [199], Event-B [83], HLPSL (High Level Protocol Specification Language) [44], Hoare logic [108], LS2 (Logic of Secure Systems) [27], LTL (linear-time temporal logic) [266], Markov Decision Process [182], Petri nets [15], π-calculus [40], PlusCal [9], Promela [172], RTL (real-time logic) [110], SPDL (Security Protocol Description Language) [168], SysML-Sec [18], TLA+ (Temporal Logic of Actions) [72], Trusted CSP# [27], überSpark [252], VDM [98], Verilog [164], VHDL [111], VML [226], vTRUST [117], XMHF (eXtensible and Modular Hypervisor Framework) [251], Z [265].

Model checkers. AVISPA (Automated Validation of Internet Security Protocols and Applications) [21], Alloy [83], CBMC (Bounded Model Checker for C and C++) [58], CWB-NC (Concurrency Workbench of New Century) [152], Cadence IFV (RTL block-level verifier) [111], FDR [103], GROOVE [102], jKind [99], NuSMV [65], OFMC (on-the-fly model checker) [34], PAT (Process Analysis Toolkit for CSP#) [237], PRISM (probabilistic model checker) [182], SATMC (SAT-based model checker for security protocols) [44], SPIN [247], TRUSTFOUND [27], UPPAAL [177], UVHM (formal analysis scheme for hypervisors) [251].

Theorem provers. Coq [72], Isabelle/HOL [144], K-framework [199], TAMARIN [154], Why [95].

Verification tools and frameworks. AndroBugs (Framework For Android Vulnerability Scanning) [241], Cl-Atse (protocol analyser) [141], FUDGE (Fuzz driver generator) [24], Frama-C [252], Krakatau [152], Maude (rewrite engine) [193], MobSF (mobile security framework) [127], phpSAFE [195], ProVerif [40], Quark [134], SAW (Software Analysis Workbench) [72], SMACK [72], SecGuru [136], SecVeriLog [92], Sugar (SAT-based) [169], TTool (translator from SysML-Sec to π-calculus) [18], Z3 [22].

这表明自Burrows等人的开创性论文[52]以来，FM在安全方面的研究和应用已经发展。我们的调查特别关注这些技术的实际应用，尤其是在工业规模上的应用。如今，一家公司如果不将其商业安全系统提交形式化分析，似乎是不可想象的。我们还怀疑黑客使用形式化技术来破解所谓的安全系统。作为最后的声明，我们需要承认调查提供了一个发展中领域的时间快照。因此，每十年需要回顾一次调查工作，我们正在计划这样做。尽管存在这个缺点，但作者认为，调查工作是研究的重要组成部分，因为它为寻找形式化方法在安全领域下的新作品和经验丰富的从业人员提供了一个起点和方向指示。

Posted 2023-01-14Updated 2023-11-27an hour read (About 8557 words)

wasm serverless edge gis

table of contents
background
serverless + gis: 现有进展
wasm + gis: 现有进展
边缘计算 + GIS？
毕设?

background

Introduce to wasm

WebAssembly(缩写 Wasm)是基于堆栈虚拟机的二进制指令格式。Wasm 是为了一个可移植的目标而设计的，可作为 C/C+/RUST 等高级语言的编译目标，使客户端和服务器应用程序能够在 Web 上部署。WASM 的运行时有多种实现，包括浏览器和独立的系统，它可以用于视频和音频编解码器、图形和 3D、多媒体和游戏、密码计算或便携式语言实现等应用。

尽管 WASM 是为了提高网页中性能敏感模块表现而提出的字节码标准, 但是 WASM 却不仅能用在浏览器(broswer)中, 也可以用在其他环境中。WASM 已经发展成为一个轻量级、高性能、跨平台和多语种的软件沙盒环境，被运用于云原生软件组件。与 Linux 容器相比，WebAssembly 的启动速度可以提高 100 倍，内存和磁盘占用空间要小得多，并且具有更好定义的安全沙箱。然而，权衡是 WebAssembly 需要自己的语言 SDK 和编译器工具链，使其成为比 Linux 容器更受限制的开发环境。WebAssembly 越来越多地用于难以部署 Linux 容器或应用程序性能至关重要的边缘计算场景。

WASM 的编译和部署流程如下：

wasm-compile-deploy

通常可以将 C/C+/RUST 等高级语言编译为 WASM 字节码，在 WASM 虚拟机中进行加载运行。WASM 虚拟机会通过解释执行或 JIT 的方式，将 WASM 字节码翻译为对应平台（ x86/arm 等）的机器码运行。

主要往三个方面:

让 C/C+ 等现有的工具和算法可以在浏览器中运行，比如 QGIS 之类的大型 GIS 桌面应用，可以达到和 native 差不多的效果；
轻量级容器：serverless，性能比现有的基于容器的 serverless 可能好很多；
边缘计算，云边协同

关于毕设, 有没有可能找一个把这几个部分都结合起来的 GIS 应用场景? serverless + edge + wasm + browser? 我调研了一下, 感觉 CS 这块有一些最新的 serverless + edge + wasm 的尝试(我自己最近也在做这些事情, 不过和 GIS 没关系), 但 GIS 好像还不是很多?

Introduce to serverless

2019年，UC伯克利大学的学者们从研究角度分析并预测，Serverless计算将取代 Serverful传统的模式，成为云计算的新一代范式。

　研究者们之所以这么说，是因为IT计算模式的变化，其实就是从Serverful计算到Serverless计算的演化。从最早的物理服务器开始，我们都在不断地抽象或者虚拟化服务器。我们使用虚拟化技术、云计算IaaS来自动管理这些虚拟化的资源。随着容器技术出现，我们用容器化CaaS实现了更轻量、更易用的虚拟化和自动化。但这些都还是从管理物理服务器到管理虚拟服务器，我们在使用时仍然需要关心背后的服务器资源分配，在程序没有使用时也需要为这些资源付费。

而现在的Serverless计算理念与技术，我们又实现了一次新的飞跃：它使得我们无需管理服务器，只需专注于业务逻辑，就可以更快构建和部署应用程序。

以一个传统Serverful应用为例：它包括业务数据等四层，为了部署这个应用，首先我们需要有一个服务器包括CPU、内存等作为计算资源，基于之上是操作系统、数据库、中间件等软件，再部署相应的业务数据等模块。如果要进行横向扩容，就需要将上述关注面复制一遍。基于容器技术，上述部署工作可以自动化，但概念模型上仍然是服务器计算资源作为基础。

而在Serverless技术支撑的应用架构中，系统四层能力都可以单独部署到可直接使用的云服务中。业务数据可以放到数据库服务中，业务逻辑执行部署到函数计算服务中。我们的服务接口可以部署到 API网关服务上，来响应动态内容的请求。静态的WebApp包部署在对象存储服务上，Web浏览器首先从对象存储中获取到应用页面本身，再发起动态请求给API网关。在这个过程中，我们使用了一系列稳定存在的云服务，并且只在使用时才计费。我们实际上只需要关注在我们的业务函数上，以及如何使用这些服务完成整个开发流程。

因此，Serverless并不意味着幕后真的没有服务器，只是服务器资源由第三方以各种专门服务的形式提供和管理，它们的资源伸缩、故障恢复等工作都由第三方也即这些BaaS/FaaS云服务提供商来负责。因此对我们应用开发者来说只需要使用这些服务即可，不再需要关心幕后的服务器。

我们可以给Serverless无服务器计算一个定义：Serverless无服务器计算是一种新的云计算模型，允许开发人员在构建和运行应用程序时，无需关心或管理服务器等基础设施。

为什么可以做到这一点？是因为云计算服务商提供了两类服务来代替服务器的作用：FaaS和BaaS。其中最关键的是FaaS，函数即服务，它是一种新的算力组织和提供方式，应用的业务逻辑被拆解为一个或多个细粒度函数，这些函数按需执行、伸缩和计费。另一类服务是BaaS，后端即服务，指的是函数执行所需要的通用的后端服务，由FaaS中的函数来按需调用。

Serverless架构对开发者意味着什么？当前，我们处于互联网分布式计算时代，默认Web BS系统，除了写出算法、读写数据，还需要考虑如何分布式部署、如何应对系统高峰时期的大并发请求；我们以AI人工智能为例，它有三个基石：算法、算力、数据。在Serverful架构中，算力由IaaS提供，算法和数据都要自行部署上去并调度管理来应对峰谷流量变化。

而在Serverless架构中，算法所需要的算力由FaaS提供，算法可以解耦成多个更细粒度的函数，开发者只需要简简单单的构思算法，即功能函数即可。数据也解耦，可以按需存储，数据的存储管理由BaaS提供。

Serverless计算尤其是FaaS函数计算，简化了计算资源的供给，极大提升了面向软件开发者的生产力，可以看作是云计算编程模型从汇编语言时代进化到高级语言时代。

基于上述分析，将Serverless无服务器计算的特征进行归纳：资源的解耦和服务化、自动弹性伸缩、按使用量计费等；相应带来的优势有低运维、低成本、高弹性、高可用等。

https://zhuanlan.zhihu.com/p/425433134

边缘计算

无服务计算，也被称为函数即服务(FAAS)，在过去两年一直是增长最快的云服务类型，仅在2019年就增长了50%。这是由于无服务计算提供了一种新的事件驱动的模型，用户可以在不关心服务配置和资源的前提下跑一些小的，无状态的应用。自动亚马逊在2014年推出了lambda，大量云服务商推出了类似的无服务平台，包括Google Cloud Functions、Microsoft Azure Functions、IBM Cloud Functions和Alibaba Cloud Functions 。虽然它们的实现各有不同，但是大多都是用虚拟机(vms)或容器作为一个沙箱环境来托管租户，并执行他们的函数。这些框架相对较重，在小内存，低延迟的场景下表现不好，尤其是这些函数第一次实例化的时候。最近的趋势和相关的技术挑战，激发了我们对边缘资源高效型无服务器计算的兴趣。其中包括以下几个：

物联网的快速发展物联网引入了大量低成本的设备，通过物理网压倒性的网络，这些设备通过不断的感知数据，产生的庞大的数据量。充分利用物联网的潜力，需要重新梳理计算模型。
依赖实时服务的新型应用程序工业物联网和下一代技术的兴起，导致计算模型需要支持极低（10ms）的延迟处理，例如：
在智慧城市中，交通灯和路灯相互通信，如果有意外发生，可以第一时间感知并响应到。
实时监控和智能视频处理功能的系统，适用于多种情况（在紧急情况下的延迟）
联网汽车并提供相关的数据服务，及时提醒司机路况危险。

这些新兴应用程序会实时的处理大量的数据。他们需要的数据处理系统具有下面的特性：低延迟开销和高系统吞吐量，多租户隔离。

在边缘侧处理数据的重要性虽然在人的认知里面，云计算是一种很好的解决方案，但是在需要无人参与的情况下能做出快速、自动化决策的场景下，依赖低延迟，它就变得没有那么好用了。例如工业控制系统中，数据分析和控制逻辑可能需要10ms以内的响应时间，上传到云端的话恐怕是不好保证这个延迟的。许多机器学习的工作负载需要在边缘场景下进行(收集传感器的数据)。但是资源和电量的限制仍然是一个挑战。为了满足以上场景的业务需求，我们必须使用新的服务来增强计算的能力，用来处理更加边缘的计算。这也就是边缘计算。

wasm + serverless + edge？

Sledge: a Serverless-first, Light-weight Wasm Runtime for the Edge

https://www2.seas.gwu.edu/~gparmer/publications/middleware20sledge.pdf

现在已经拥有了很多无服务器（serverless）的商业、开源平台，但是这些利用虚拟机和容器的解决方案对于资源有限的边缘系统来说过于重了，调度容器（冷启动）、启动一个虚拟机，往往需要大量的内存占用和很高的调用时间。另外，无服务的工作负载，主要的关注在每个客户端的请求，短期运行的计算并不适合常规的计算系统。

在本文中，我们设计和实现了一种新颖高效的基于WebAssembly的edge框架—sledge。Sledge的经过一些优化以面对独特属性的工作负载：多租户的，启动快的，突发的客户端请求以及短期的计算。

在本文章中，我们展示Sledge的设计和实现–一种新颖的、基于WebAssembly的、高效的边缘serverless框架。Sledge主要优化并且支持了一些独特场景的工作负载：高密度的租户，短启动时间，突发的客户端请求和短期计算。Sledge通过优化调度来解决短期计算和有效的任务分配，轻量级的函数隔离模型来实现基于WebAssembly的故障隔离。这些轻量的沙箱目标是在高密度计算：为了高密度的客户端请求，快速吊起和释放函数。和其它真实世界serverless运行时对比，在工作负载多变的条件下，设计一个边缘优先的serverless框架是有效的。与 Nuclio 相比，Sledge 支持4倍的吞吐量，延迟降低了4倍，是其中最快的serverless框架之一。
Evaluating webassembly enabled serverless approach for edge computing：

Evaluating webassembly enabled serverless approach for edge computing

Abstract:

The edge computing ecosystem has been evolving in the last few years. There have been different architectural patterns proposed to implement edge computing solutions. This paper focuses on serverless edge computing architecture and evaluates webassembly based approach for the same. The current state of serverless edge computing is explained followed by providing high level conceptual overview of webassembly. Webassembly performance is evaluated against native and container based applications using the current toolchain supported for ARM architecture. Benchmarking is done for different categories of applications like compute intensive, memory intensive, file I/O intensive and a simple image classification - machine learning application. This paper describes the experimental setup, discusses the performance results and provides the conclusion.

Published in: 2020 IEEE Cloud Summit
WearMask: Fast In-browser Face Mask Detection with Serverless Edge Computing for COVID-19

https://arxiv.org/abs/2101.00784

COVID-19的流行一直是美国的一个重大医疗挑战。根据美国疾病控制和预防中心（CDC）的资料，COVID-19感染主要是通过人们呼吸、说话、咳嗽或打喷嚏时产生的呼吸道飞沫传播。戴口罩是阻挡80%的呼吸道感染的主要、有效和方便的方法。因此，许多口罩检测和监测系统已经被开发出来，为医院、机场、出版物运输、运动场所和零售场所提供有效的监督。然而，目前的商业口罩检测系统通常与特定的软件或硬件捆绑，阻碍了公众的使用。在本文中，我们提出了一个基于浏览器的无服务器边缘计算的人脸面具检测解决方案，称为基于网络的高效人工智能面具识别（WearMask），它可以部署在任何有互联网连接的普通设备（如手机、平板电脑、电脑）上，使用网络浏览器，而无需安装任何软件。无服务器的边缘计算设计最大限度地减少了额外的硬件成本（例如，特定的设备或云计算服务器）。所提出的方法的贡献在于提供了一个整体的边缘计算框架，它整合了（1）深度学习模型（YOLO），（2）高性能神经网络推理计算框架（NCNN），和（3）基于堆栈的虚拟机（WebAssembly）。对于终端用户来说，我们基于网络的解决方案具有以下优势：（1）无服务器边缘计算设计，设备限制和隐私风险最小；（2）免安装部署；（3）计算要求低；（4）检测速度高。我们的WearMask应用程序已经在这个http URL上推出，供公众访问。

serverless + gis: 现有进展

胡中南：云原生GIS 2.0新技术解读之Serverless + GIS：http://stock.10jqka.com.cn/20220908/c641712842.shtml
SuperMap GIS 11i(2022) 新特性速览：https://www.supermap.com/zh-cn/a/product/11i-characteristic-2022.html
SuperMap GIS 11i(2022)正式发布，揭秘七大特性：https://baijiahao.baidu.com/s?id=1737120191867774649&wfr=spider&for=pc
Geospatial Serverless Computing: Architectures, Tools and Future Directions

https://www.researchgate.net/publication/341245906_Geospatial_Serverless_Computing_Architectures_Tools_and_Future_Directions

Several real-world applications involve the aggregation of physical features corresponding to different geographic and topographic phenomena. This information plays a crucial role in analyzing and predicting several events. The application areas, which often require a real-time analysis, include traffic flow, forest cover, disease monitoring and so on. Thus, most of the existing systems portray some limitations at various levels of processing and implementation. Some of the most commonly observed factors involve lack of reliability, scalability and exceeding computational costs. In this paper, we address different well-known scalable serverless frameworks i.e., Amazon Web Services (AWS) Lambda, Google Cloud Functions and Microsoft Azure Functions for the management of geospatial big data. We discuss some of the existing approaches that are popularly used in analyzing geospatial big data and indicate their limitations. We report the applicability of our proposed framework in context of Cloud Geographic Information System (GIS) platform. An account of some state-of-the-art technologies and tools relevant to our problem domain are discussed. We also visualize performance of the proposed framework in terms of reliability, scalability, speed and security parameters. Furthermore, we present the map overlay analysis,point-cluster analysis, the generated heatmap and clustering analysis. Some relevant statistical plots are also visualized. In this paper, we consider two application case-studies. The first case study was explored using the Mineral Resources Data System (MRDS) dataset, which refers to worldwide density of mineral resources in a country-wise fashion. The second case study was performed using the Fairfax Forecast Households dataset, which signifies the parcel-level household prediction for 30 consecutive years. The proposed model integrates a serverless framework to reduce timing constraints and it also improves the performance associated to geospatial data processing for high-dimensional hyperspectral data.

wasm + gis: 现有进展

GIS Processing on the Web

https://www.diva-portal.org/smash/record.jsf?pid=diva2%3A1674422&dswid=6199

Today more and more advanced and demanding applications are finding their way to the web. These are applications like video editing, games, and mathematical calculations. Up until a few years ago, JavaScript was the only language present on the web. That was until Mozilla, Google, Microsoft, and Apple decided to develop WebAssembly. WebAssembly is a low-level language, similar to assembly, but running in the browser. WebAssembly was not created to replace JavaScript, but to be used alongside it and complement JavaScript’s weaknesses. WebAssembly is still a relatively new language (2017) and is in continuous development. This work is presented as a guideline, and to give a general direction of how WebAssembly is performing (in 2022) when operating on GIS data.

今天，越来越多的先进和高要求的应用程序正在找到它们的方式，在网络上。这些应用包括视频编辑、游戏和数学计算等。直到几年前，JavaScript是网络上唯一存在的语言。直到Mozilla、谷歌、微软和苹果决定开发WebAssembly。WebAssembly是一种低级语言，类似于汇编，但在浏览器中运行。创建WebAssembly不是为了取代JavaScript，而是为了与它一起使用，补充JavaScript的弱点。WebAssembly仍然是一种相对较新的语言（2017年），并且正在不断发展。这项工作是作为一个指南提出的，并给出了WebAssembly在GIS数据上运行时的总体表现方向（2022年）。
The US COVID Atlas: A dynamic cyberinfrastructure surveillance system for interactive exploration of the pandemic

Distributed spatial infrastructures leveraging cloud computing technologies can tackle issues of disparate data sources and address the need for data-driven knowledge discovery and more sophisticated spatial analysis central to the COVID-19 pandemic. We implement a new, open source spatial middleware component (libgeoda) and system design to scale development quickly to effectively meet the need for surveilling county-level metrics in a rapidly changing pandemic landscape. We incorporate, wrangle, and analyze multiple data streams from volunteered and crowdsourced environments to leverage multiple data perspectives. We integrate explorative spatial data analysis (ESDA) and statistical hotspot standards to detect infectious disease clusters in real time, building on decades of research in GIScience and spatial statistics. We scale the computational infrastructure to provide equitable access to data and insights across the entire USA, demanding a basic but high-quality standard of ESDA techniques. Finally, we engage a research coalition and incorporate principles of user-centered design to ground the direction and design of Atlas application development.

From an infrastructure perspective, the Atlas is the first web application (to our knowledge) that integrates WebAssembly technology to manage computationally intensive spatial analysis functions (written in C++) directly in the web browser, opening wide new possibilities of browser-based geoprocessing and GIScience.

从基础设施的角度来看，Atlas是第一个集成了WebAssembly技术的网络应用程序（据我们所知），可以直接在网络浏览器中管理计算密集型的空间分析功能（用C++编写），为基于浏览器的地理处理和GIS科学提供了广泛的新可能性。
新一代三维GIS技术体系: 超图

https://www.supermap.com/zh-cn/a/product/11i-tec-3-2022.html

发布自主研发的全新 WebGL 三维客户端：
- 完善 Web 端的三维渲染引擎，支持更强的粒子系统、更多光影特效、更多后处理特效、更具真实感的物理材质
- 支持游戏引擎导出的标准 PBR 材质，复制游戏引擎美化后的三维场景
- 基于 WebAssembly 技术，支持直接加载 .x、.dae 等更多三维模型格式的数据
- 提供 Vue2.0/3.0 开发组件，支持低代码开发
WebAssembly4G: Where we are, and where we’re heading

https://talks.osgeo.org/foss4g-2022/talk/ASDL7P/

WebAssembly’s adoption is gaining traction and still, its potential is not yet fully utilized, especially for the processing and visualization of geo data in and outside of browsers. In this session I will give a technical introduction to WebAssembly. I will show its current state and adaptation in FOSS4G projects and will talk about the ongoing advancements of the technology and possible future scenarios.

This will also be a hands-on session, where after showing how to get up and running, I will share my experience, tips and tricks collected while porting the latest versions of GEOS, PROJ, GDAL, SpatiaLite and osgEarth to the web platform.

The composition of existing OSGeo/FOSS C/C++ libraries in a portable and sandboxed form also brings many advantages outside of browsers. The talk will close with some demos about how WebAssembly enables us to build for the web, as well as for any other platform.

WebAssembly的采用越来越多，但它的潜力仍未得到充分的利用，特别是在浏览器内外的地理数据的处理和可视化方面。在这次会议上，我将对WebAssembly做一个技术介绍。我将展示它的现状和在 FOSS4G 项目中的适应性，并将谈论该技术的持续进步和未来可能的情况。这也将是一个实践会议，在展示了如何启动和运行之后，我将分享我在将GEOS、PROJ、GDAL、SpatiaLite和osgEarth的最新版本移植到网络平台时收集的经验、技巧和窍门。现有的OSGeo/FOSS C/C++库以可移植和沙盒的形式组成，在浏览器之外也带来了许多优势。讲座的最后会有一些演示，介绍WebAssembly如何使我们为网络以及其他平台进行构建。
Write once, run anywhere: safe and reusable analytic modules for WebAssembly, Javascript, or more!

https://talks.osgeo.org/foss4g-2022/talk/XV87XB/

The proliferation of client-side analytics and on-going vulnerabilities with shared code libraries have fueled the need for better safety standards for running executables from potentially unknown sources. WebAssembly (WASM), a compilation target that allows lower-level languages like Rust, C, and Go to run in the browser or server-side at near-native speeds. Much like Docker changed the way we run virtualized workflows, WASM runtimes create safe virtual environments where access to the host system is limited.
In combination with a new free and open source full-stack geospatial platform, Matico, efforts are underway to enable portability across workflows and applications to more easily use WASM modules. WASM implementations of GDAL are in the works, and powerful open source Rust geospatial libraries are easily packaged for web usage through Wasm-Pack. Additional geo WASM libraries like jsgeoda provide spatial indices, binning, and autocorrelation functions. Shareable code can be a recipe for security vulnerabilities and attack vectors, potentially exposing personal or critical information, particularly if there is the opportunity to run code server-side. WASM implementation alleviates this by requiring access from the Virtual Machine (VM) to be limited and explicit, and for Javascript developers the lightweight AssemblyScript language is relatively familiar.
An upcoming Javascript feature called ShadowRealms may enable even simpler and more familiar implementations to safely run Javascript code shared between module authors. These developments lay the groundwork for a hybrid front- and backend geospatial ecosystem of shareable code snippets and analytic functions, much like have emerged in the UI component Javascript ecosystem. The combination of emerging features positions web geospatial analytics and This talk explores the implementation and performance of running geospatial analytic modules through a WebAssembly virtual machine and through the upcoming Javascript ShadowRealm specification.

客户端分析的激增和共享代码库的持续漏洞，促使人们需要更好的安全标准来运行来自潜在未知来源的可执行文件。WebAssembly（WASM）是一个编译目标，允许Rust、C和Go等低级语言以接近原生的速度在浏览器或服务器端运行。就像Docker改变了我们运行虚拟化工作流程的方式一样，WASM运行时创建了安全的虚拟环境，对主机系统的访问受到限制。

结合新的免费和开源的全栈地理空间平台Matico，正在努力实现跨工作流程和应用程序的可移植性，以更容易地使用WASM模块。GDAL的WASM实现正在进行中，强大的开源Rust地理空间库可以通过Wasm-Pack轻松打包供网络使用。额外的地理WASM库，如jsgeoda，提供空间指数、分档和自相关功能。可共享的代码可能是安全漏洞和攻击载体的秘诀，有可能暴露个人或关键信息，特别是如果有机会在服务器端运行代码。WASM的实施通过要求来自虚拟机（VM）的访问是有限的和明确的，而对于Javascript开发者来说，轻量级的AssemblyScript语言是相对熟悉的，从而缓解了这种情况。

一个即将到来的名为ShadowRealms的Javascript功能可能使更简单和更熟悉的实现安全地运行模块作者之间共享的Javascript代码。这些发展为可共享的代码片段和分析功能的前后端地理空间混合生态系统奠定了基础，就像UI组件Javascript生态系统中出现的那样。新兴功能的结合，使网络地理空间分析和本讲座探讨了通过WebAssembly虚拟机和即将推出的Javascript ShadowRealm规范运行地理空间分析模块的实现和性能。
https://github.com/stuartlynn/wasm_geo_agg

Wasm Geo Agg is a proof of concept to explore performing complex geospatial operations in the browser using Rust and WebAssembly. As an initial test, we are focusing on point in polygon operations. Simply load in a CSV file with points and a GeoJSON file with polygons then click aggregate.

Currently, if you want to process geospatial data you can either
1. Spend a day or two installing a bunch of really amazing tools like GDAL, PostGIS, QGIS etc and banging your head a few times as you try to get all their versions compatible with each other ( not to mention trying to not blow up your python installation as you go)
2. Learn Python or R and use packages like geopandas
3. Upload your data to services like ArcGis or CARTO to be stored and processed in the cloud somewhere.
Options 1 or 2 let you process data locally but have a steep learning curve. As someone who has been working in the geospatial world for 4+ years, I still lose half a day each time I need to install a new geospatial stack. While using something like docker makes this a little easier, that too has a bit of a learning curve.

Option 3 means that you to some extent hand over control of your data to a third party. If the data is sensitive and needs to remain local (as is true for a lot of non-profits or research data), or if you need a service that can be guaranteed to still be around in 5-10 years, these options might not be ideal either. Another consideration is that the cloud servers that process the data on these services are often less powerful than the laptop you are using to read this article, which increasingly seems insane to me.

So this is an experiment exploring a 4th option. To ask: what if we had a PostGIS that ran entirely in your browser? A system that uses the web to deliver sophisticated software to your computer in the form of javascript and WASM with zero installation overhead, that then processes your data locally using the powerful CPU that happens to live in your machine.
ArcGIS API for JavaScript and WebAssembly

https://developers.arcgis.com/javascript/latest/faq/

Does the ArcGIS API for JavaScript support all Content Security Policy directives?

No. Most CSP directives are supported and certified within the ArcGIS for JavaScript API. The API’s 3D functionality, in addition to the projection engine, makes use of WebAssembly (wasm). Wasm requires unsafe-eval in the script-src directive. Adding this in CSP goes against the protection that it is supposed to provide. There is a WebAssembly GitHub proposal that discusses this in more detail. Until this is addressed, applications that make use of these two parts of the API will not be able to take advantage of using CSP.

看起来这里也用了 wasm，不过这个是不是不开源？
QGIS-Developer QGIS and WebAssembly - OSGeo mailing list
- https://lists.osgeo.org/pipermail/qgis-developer/2022-March/064589.html
- https://wonder-sk.github.io/wasm/qgis.html
  
  跑在浏览器里面的 QGIS

边缘计算 + GIS？

边缘计算GIS技术指的是将边缘计算的各种特征，用于支撑GIS应用的各要素，包括GIS内容的发布和分发，GIS服务的代理和加速，以及在线分析和计算，以一种更加灵活的方式，高效率、低成本地使用地理信息资源。

边缘计算GIS技术是云GIS技术的重要的补充，具体包括以下技术：

边缘前置代理：在GIS云中心和客户端之间，对GIS服务进行代理加速，提供更好的服务访问体验。
边缘服务聚合：将不同来源，不同内容的GIS服务聚合为一个服务，实现多源、异构地理信息与服务的整合。
边缘内容分发：云GIS中心自动将瓦片数据分发到边缘GIS节点，实现了边缘GIS内容的自动更新。
边缘分析计算：在边缘端按需进行GIS分析和计算，有效提升GIS服务性能。
为什么我们需要边缘计算GIS技术？ https://baijiahao.baidu.com/s?id=1718990389366964311&wfr=spider&for=pc
边缘计算GIS技术篇——边缘GIS再升级，满足云-边-端架构GIS应用多重需求： https://magazine.supermap.com/view-1000-15938.aspx

参考论文: WASM/eBPF + Serverless

SPRIGHT: Extracting the Server from Serverless Computing! High performance eBPF-based Event-driven, Shared-memory Processing

https://dl.acm.org/doi/10.1145/3544216.3544259

Serverless computing promises an efficient, low-cost compute capability in cloud environments. However, existing solutions, epitomized by open-source platforms such as Knative, include heavyweight components that undermine this goal of serverless computing. Additionally, such serverless platforms lack dataplane optimizations to achieve efficient, high-performance function chains that facilitate the popular microservices development paradigm. Their use of unnecessarily complex and duplicate capabilities for building function chains severely degrades performance. ‘Cold-start’ latency is another deterrent.

We describe SPRIGHT, a lightweight, high-performance, responsive serverless framework. SPRIGHT exploits shared memory processing and dramatically improves the scalability of the dataplane by avoiding unnecessary protocol processing and serialization-deserialization overheads. SPRIGHT extensively leverages event-driven processing with the extended Berkeley Packet Filter (eBPF). We creatively use eBPF’s socket message mechanism to support shared memory processing, with overheads being strictly load-proportional. Compared to constantly-running, polling-based DPDK, SPRIGHT achieves the same dataplane performance with 10× less CPU usage under realistic workloads. Additionally, eBPF benefits SPRIGHT, by replacing heavyweight serverless components, allowing us to keep functions ‘warm’ with negligible penalty.

Our preliminary experimental results show that SPRIGHT achieves an order of magnitude improvement in throughput and latency compared to Knative, while substantially reducing CPU usage, and obviates the need for ‘cold-start’.

SPRIGHT利用共享内存处理，并且戏剧性的通过避免没必要的协议处理和序列化/反序列化开销，提升了数据面的扩展性。SPRIGHT广泛地使用eBPF进行事件驱动的处理。作者创造性的使用eBPF的socket消息机制来支持共享内存处理，其开销严格的与负载成比例。在真实的负载下，与不间断的运行、基于轮询的DPDK相比，SPRIGHT能够在使用10倍少的CPU使用量的情况下，实现相同的数据面性能。除此之外，eBPF通过代替重量级的无服务组件让SPRIGHT变好，让作者能够在开销可以忽略的情况下，保持函数“暖”（warm）。作者的初步实验结果表明，与Knative相比，SPRIGHT在吞吐和时延上有一个数量级的提升，同时实质上减少了CPU的用量，并且避免了“冷启动”的需求。

SIGCOMM ‘22: Proceedings of the ACM SIGCOMM 2022 Conference
Sledge: A serverless-first, light-weight wasm runtime for the edge

https://dl.acm.org/doi/abs/10.1145/3423211.3425680
Faasm: Lightweight Isolation for Efficient Stateful Serverless Computing

Serverless computing is an excellent fit for big data processing because it can scale quickly and cheaply to thousands of parallel functions. Existing serverless platforms isolate functions in ephemeral, stateless containers, preventing them from directly sharing memory. This forces users to duplicate and serialise data repeatedly, adding unnecessary performance and resource costs. We believe that a new lightweight isolation approach is needed, which supports sharing memory directly between functions and reduces resource overheads.

We introduce Faaslets, a new isolation abstraction for high-performance serverless computing. Faaslets isolate the memory of executed functions using \emph{software-fault isolation} (SFI), as provided by WebAssembly, while allowing memory regions to be shared between functions in the same address space. Faaslets can thus avoid expensive data movement when functions are co-located on the same machine. Our runtime for Faaslets, Faasm, isolates other resources, e.g. CPU and network, using standard Linux cgroups, and provides a low-level POSIX host interface for networking, file system access and dynamic loading. To reduce initialisation times, Faasm restores Faaslets from already-initialised snapshots. We compare Faasm to a standard container-based platform and show that, when training a machine learning model, it achieves a 2× speed-up with 10× less memory; for serving machine learning inference, Faasm doubles the throughput and reduces tail latency by 90%.

https://arxiv.org/abs/2002.09344

Shillaker S, Pietzuch P. Faasm: Lightweight isolation for efficient stateful serverless computing[C]//2020 {USENIX} Annual Technical Conference ({USENIX}{ATC} 20). 2020: 419-433.

毕设?

希望往 wasm + eBPF + edge computing + serverless + gis 的方向走?
尝试有一些相关的 gis 的 demo 应用, 证明这个思路的可行性?
在浏览器里面运行的大型 GIS 应用程序和分析程序, 同时还可以通过云端加速? (云边协同?)
比如同样一个 function, 又可以跑在浏览器里面, 又可以跑在边缘计算的节点, 又可以在云上以 serverless 的方式扩容, 同时性能还不错? 可以用任意语言编写, 也不需要管理对应的调度复杂度, 还可以并行?
什么样的 GIS 应用场景比较好呢? 我目前没想到….总之就是做一个 showcase, 证明这个思路的可行性, 以及有一些应用场景的潜力?
- 要有现成的开源代码, 最好是 C/C++ 写的, Java 或者 Go 可能也勉强可以, 这样我不用自己写太具体的 GIS 算法, 只要搭框架和写业务就好(这样工作量不至于过大); 而且我和华南理工那边都希望开源出去;
- 最好是计算密集型, 但还是有一定程度上的相互通信的科学计算任务, 比较方便展示 serverless 并行效果?(图形学的事可能不如用 GPU 跑)
- 或者原先是桌面的 C/C++ 算法代码, 现在编译成 wasm 就可以丢进浏览器跑, 同时还可以上云扩容?以及在浏览器里面跑, 还可以糊一个前端,看起来好玩一点?
- 有一些边缘计算场景?
具体的工作的话我也可以去修改一下这个底层的 wasm serverless 运行时平台, 然后把这个 GIS 的工作负载应用给跑上去.
校外导师?

(不知道, 瞎说的)

dlsym

摘要（中文）

Abstract （英文）

目录

绪论

1.1 研究背景与意义

1.2 国内外研究现状

云计算与时空数据分析研究现状

WebGIS 与 WebAssembly 技术研究现状

1.3 论文研究内容

1.4 论文章节安排

相关技术介绍与分析

2.1 云原生技术的发展与挑战

2.2WebGIS 技术的的发展与挑战

WebAssembly 技术

应用移植 WebAssembly 平台流程概述

Wasm 与 JavaScript 在时空数据分析中的性能对比

2.3 Wasm与云原生技术如何解决 WebGIS 的挑战

3 GPlates软件的重构与迁移

3.1 GPlates软件简介

3.1.1 GPlates 软件功能

3.1.2 GPlates 板块运动模型

3.1.3 GPlates 现有生态的不足和改进空间

3.2GPlates 2.3.0软件结构分析与移植挑战

GPlates 2.3.0软件结构分析

3.2.2 移植 GPlates 面对的挑战

3.3GPlates 到 WebAssembly 的移植与重构

WebAssembly 环境准备与依赖库构建

3.3.2 GPlates 重构与移植

3.4 GPlates 功能测试

4基于无服务器计算的GPlates服务实现

4.1设计与实现基于无服务器计算的 GPlates 服务

需求分析

系统架构设计

前端界面布局设计与实现

前端可视化设计与实现

API 网关与函数即服务设计与实现

数据存储与访问设计实现

用户认证与授权设计实现

4.2部署与优化

4.3性能与资源消耗评估

5 结论与展望

5.1研究存在的问题与展望

5.2研究结论

参考文献

从OpenAI的Codex模型到GitHub Copilot

为什么上下文很重要

GitHub Copilot 如何理解您的代码

提高语义理解能力

片段A：

片段B：

片段C：

总结与回顾

了解更多

插件清单

OpenAPI 定义

运行插件

编写插件描述

最佳实践

调试插件

开发模板

参考资料

动机

本地代码类比

组件 <-> 可执行文件

模块 <-> 共享库

组件实例 <-> 进程

模块实例 <-> 已加载的共享库

Wasm运行时 <-> 操作系统

注意事项

（借用的）可视化

结论

组件模型的描述文件 - WIT

如何在实际项目中使用 WIT 开发 Wasm 组件

示例

不同语言编写的 Wasm 组件协同工作

btf2wit

Rust + wit-bingen

关于WIT和组件模型的更多信息

参考资料