使用Checked C重构FreeBSD内核：安全与效率的双赢

39 浏览量更新于2024-08-25 收藏 192KB PDF 举报

"Refactoring the FreeBSD Kernel with Checked C - 2020 是一篇由 Junhan Duan、Yudi Yang、Jie Zhou 和 John Criswell 等人撰写的计算机科学论文，发表于罗切斯特大学计算机科学系。该研究关注了现代操作系统内核普遍采用C语言编程的问题，这使得它们易受缓冲区溢出和缓冲区读取攻击。Microsoft针对这一问题开发了一种名为Checked C的C语言扩展，通过静态分析和运行时检查插入，旨在防止空指针解引用和空间内存安全错误。文章的核心内容是作者们对FreeBSD内核代码的重构实践，他们将部分系统调用实现、UDP和IP网络功能的代码转换为使用Checked C特性。重构工作由两名研究生历时约三个月完成，包括系统调用处理、网络包（mbuf）实用程序以及IP和UDP处理代码。研究发现，尽管进行了这样的改造，Checked C并未带来显著的性能损失或代码大小增加，证明了这种安全增强技术在实际操作系统的可接受性。通过这项实证研究，作者们评估了Checked C在操作系统内核中的适用性和效率，为其他开发者提供了一个关于如何在保证代码安全性的前提下进行代码重构的案例。这对于理解如何在现代操作系统开发中平衡安全和性能具有重要意义，特别是对于那些致力于提高系统稳定性和减少潜在安全漏洞的开发者来说，Checked C提供了一种值得考虑的解决方案。" 本文不仅探讨了技术细节，还强调了在实际项目中的实施步骤和结果，为软件工程实践者提供了有益的经验教训，尤其是在处理关键系统代码时如何采用更安全的编程语言特性。这篇论文是关于C语言安全改进、系统级代码重构和性能评估的重要参考资料。

Refactoring the FreeBSD Kernel with Checked C

Junhan Duan,

∗

Yudi Yang,

∗

Jie Zhou, and John Criswell

Department of Computer Science

University of Rochester

Abstract—Most modern operating system kernels are written

in C, making them vulnerable to buffer overﬂow and buffer

over-read attacks. Microsoft has developed an extension to the

C language named Checked C which provides new source

language constructs that allow the compiler to prevent NULL

pointer dereferences and spatial memory safety errors through

static analysis and run-time check insertion. We evaluate the use

of Checked C on operating system kernel code by refactoring

parts of the FreeBSD kernel to use Checked C extensions. We

describe our experience refactoring the code that implements

system calls and UDP and IP networking. We then evaluate the

refactoring effort and the performance of the refactored kernel.

It took two undergraduate students approximately three months

to refactor the system calls, the network packet (mbuf) utility

routines, and parts of the IP and UDP processing code. Our

experiments show that using Checked C incurred no performance

or code size overheads.

Index Terms—memory safety, safe C, FreeBSD

I. INTRODUCTION

Most modern operating system (OS) kernels, such as

Linux [14] and FreeBSD [39], are implemented in C. However,

due to C’s lack of memory safety and type safety, OS kernels

written in C can have exploitable memory safety errors. These

memory safety errors may lead to the kernel having denial of

service (DoS) [3], [4], [6], [8], privilege escalation [4], [8], and

arbitrary code execution [6], [7] vulnerabilities. Memory safety

errors in OS kernels are extremely dangerous as kernels form

the foundation of the entire software stack; successful exploita-

tion of kernel memory safety errors can lead to memory cor-

ruption and information disclosure [16]. Such attacks can even

bypass defenses such as Data Execution Prevention (DEP) [2]

and Address Space Layout Randomization (ASLR) [19], [41].

To mitigate these vulnerabilities, one could rewrite the

OS kernel in a safe language; examples include Singular-

ity [30] (Sing# [26]), Mirage [38] (OCaml), Redox [24] and

Tock [36] (Rust), and Biscuit [23] (Go). However, rewriting

the OS kernel requires signiﬁcant programmer effort. Another

approach is to use automatic compiler transformations to

enforce memory safety [21], [22] or Control Flow Integrity

(CFI) [9]. Memory safety transformations on kernel code

have high overhead (some kernel latency increase by as much

as 35× [21]) while CFI approaches [20], [27], [29] fail to

mitigate non-control data attacks [17].

Checked C [25], [44] is a new safe C dialect from Microsoft

that extends the C language with new pointer types for which

the compiler automatically performs NULL pointer checks and

array bounds checks; the compiler either proves that use of the

∗

Junhan Duan and Yudi Yang are co-primary authors.

pointer is safe at compile time or inserts run-time checks to

ensure safety at run-time. Checked C has low performance

overhead (only 8.6% on selected benchmarks [25]), and its

spatial safety checks mitigate both control-data [43], [48] and

non-control data [17] attacks.

In this paper, we investigate the use of Checked C in

refactoring parts of an OS kernel to be spatially memory

safe. Speciﬁcally, we quantify the performance and code size

overheads of using Checked C on OS kernel code and identify

challenges and solutions to using Checked C on OS kernel

code. We chose FreeBSD 12 stable to harden with Checked C

as FreeBSD uses Clang and LLVM [35] as its default compiler;

Checked C is based on Clang and LLVM [25]. Since there are

millions of lines of code inside the FreeBSD kernel, we refac-

tored kernel components that we think are part of the kernel’s

attack surface. Speciﬁcally, we refactored code that copies

data between application memory and kernel memory i.e.,

code using the copyin() and copyout() functions [5],

as such code, if incorrect, would allow applications to read

or corrupt the OS kernel’s memory. We also refactored code

in the TCP/IP stack as the TCP/IP stack processes data from

untrusted networks. Speciﬁcally, we modiﬁed the mbuf utility

routines [46] which manipulate packet headers and parts of the

UDP and IP processing code.

The rest of this paper is organized as follows: Section II

provides background on Checked C. Section III describes the

threat model. Section IV discusses how we refactored the

FreeBSD kernel to use Checked C features. Section V dis-

cusses our refactoring efforts. Section VI presents the results of

our evaluation on the refactored FreeBSD kernel. Section VII

discusses related work, and Section VIII concludes.

II. BACKGROUND ON CHECKED C

Checked C [25], [44] is a new safe C dialect. Checked C’s

design distinguishes itself from previous safe-C works [18],

[32], [34] in that it enables programmers to easily convert

existing C code into safe Checked C code incrementally, and it

maintains high backward compatibility. Currently, Checked C

provides no temporal memory safety protections, so our work

does not discuss temporal memory safety. In this section,

we brieﬂy introduce Checked C’s key features: new types of

pointers (Section II-A), checked regions (Section II-B), and

bounds-safe interfaces (Section II-C).

A. New Pointer Types

Checked C extends C with three new types of pointers

for spatial memory safety: ptr<T>, array_ptr<T>, and

下载后可阅读完整内容，剩余7页未读，立即下载

weixin_38570406

粉丝: 9
资源: 951

使用Checked C重构FreeBSD内核：安全与效率的双赢

Refactoring2-free-chapter_cn.pdf

Subspace-tracking-refactoring.rar_perception_subspace

pfwtfp-refactoring-with-the-master-lab-atlanta-web-100719-gap

pfwtfp-refactoring-with-the-master-lab-dumbo-web-010620-mod-1-repeat

lseudo-Refactoring.rar_文件操作_Visual_Basic_

curtor-Refactoring.rar_Windows编程_Borland_C++_

06-18-20_Refactoring：将教程代码转换为完善的代码

java笔试题算法-php-finder_refactoring-kata::elephant::magnifying_glass_tilted_left:难懂的Finder重构PHPKata端口

refactoring-improving-the-design-of-existing-code:改进改善既有代码的设计源代码

Refactoring-Improving-the-Design-of-Existing-Code:et《重建:label:改善既有代码的设计》

最新资源