Coq：世界上最好的宏汇编器？（2013）

导读

这篇论文探讨能否把 Coq 当作“世界上最好的宏汇编器”来使用：在 Coq 中形式化 x86 汇编子集的语义，并借助宏和类型系统编写底层程序，同时证明这些程序的性质。评论者认为它属于“认证程序”（certified programs）研究路线，展示了用证明助理进行汇编级验证的可行性。

HN 关注点：Coq 用于汇编级程序验证的潜力，以及形式化方法能否提升底层系统软件可靠性；讨论也延伸到认证程序研究和 Coq 的命名梗。

关键词　Coqformal verificationassemblyx86

HN 评论精选

这几条评论里：支持 1　补充 2

支持盛赞 Coq 与类型论的教育价值，认为以函数式编程和逻辑为基础能显著提升软件质量，并顺带吐槽语言名字。

Coq 是一门了不起的语言。学习使用它并理解其背后的理论，会让人对计算机科学有更丰富、更深刻的理解。这个意义上它类似 Haskell，但类型系统更强大（强大得多！）。我还是初学者，但即便经验有限也觉得耳目一新。我希望逻辑、类型论和函数式编程成为计算机科学教育的基础，而不是相对晦涩笨重的面向对象和命令式范式；我相信软件质量会因此大幅提升。（是的，它的名字确实很不幸，尤其当面讨论时很难不笑；读作“coke”有帮助，但仍是房间里的大象。另外我不确定 PDF 叫 coqasm 是双关还是巧合。）

thinkpad20查看英文原文

Coq is an amazing language. Learning to use it, and understanding the theories that underpin it, give one a far richer sense of understanding of computer science. In that sense it's akin to Haskell, but with an even more (much more!) powerful type system. I'm still a beginner but even with my limited expertise, it's a real breath of fresh air. I would love to see a world in which logic, type theory and functional programming formed the foundation of computer science education, rather than the comparatively arcane and clunky paradigms of object-oriented and imperative programming. I'm convinced that the quality of software would improve drastically. (And yes, its name is truly unfortunate. It's hard to have a conversation about the language, especially in person, without giggling over the name. Pronouncing it "coke" helps, but it's still the elephant in the room.) (Also, I'm not sure if the fact that this pdf is entitled "coqasm" is a pun or an amusing coincidence.)

补充补充认证程序的研究路线和 C 子集形式化例子，说明形式化 x86 子集为何有价值。

如果其他人也感兴趣，认证程序（certified programs）有一条类似的研究路线：先在 Coq 中规定某种语言的语义，再用该语言写程序，这样就能在 Coq 中分析程序并证明某些性质。流程大致是：语言 -> Coq -> 证明性质。另一个例子是 Sandrine Blazy 和 Xavier Leroy 把 C 的一个子集形式化到 Coq 中（Clight）。StackOverflow 上也有关于“认证程序”定义的讨论。总之，在 Coq 中形式化 x86 架构的一个子集，意味着可以用 Coq 证明汇编程序的性质，这既有趣又令人印象深刻。

kxyvr查看英文原文

In case someone else is interested in this kind of work, there's an interesting line of research in certified programs that's similar to this. Basically, you specify the semantics of some language in Coq. Then, write a program in the desired language. This allows us to analyze the program in Coq and prove certain properties about it. Essentially, it's a process to develop certified programs by using the process: language -> Coq -> prove properties As another example of this, Sandrine Blazy and Xavier Leroy have a paper that formalize a subset of C in Coq: http://pauillac.inria.fr/~xleroy/publi/Clight.pdf There's also some discussion on StackOverflow about the definition of what a certified program is: https://stackoverflow.com/questions/21320138/definition-of-a-certified-program In any case, formalizing a subset of the x86 architecture in Coq means that we can prove properties about a program written in assembler using Coq, which is both interesting and impressive.

补充从宏汇编器和 Forth 的错误处理谈起，强调需要更强验证来排除内存泄漏、注入、DoS 等问题，并指出大量基础软件用 C/C++ 缺乏内存安全。

这是个很有趣、很发人深省的想法。写 httpdito、尤其把一个小型 peephole optimizer 做成 gas 宏时，我意识到一些 Forth 系统非常接近宏汇编器；而不用高级语言而用宏汇编器的唯一原因，是宏汇编器和 Forth 的错误处理极差甚至几乎没有。动态类型语言能较高保证程序不崩溃，强静态类型语言则通过编译期检查提供类似但较弱的保证；但程序员显然还需要验证程序没有内存泄漏、无限循环、SQL 注入、XSS、CSRF、billion-laughs 式 DoS 等问题，更不用说 Flexcoin 因使用非事务性数据存储而破产这类问题。与此同时，我们日常软件中的很大一部分（X11、Firefox、Emacs、Apache、内核，以及臭名昭著的 OpenSSL）是用 C/C++ 写的，连基本的内存安全都缺乏。

kragen查看英文原文

Quoting my comment on this paper from 8 months ago on https://lobste.rs/s/pc1v4g/coq_the_world_s_best_macro_assembler_microsoft_research, where it is full of links to the things I'm referring to: This is a really interesting and thought-provoking idea. In writing httpdito, and in particular in putting a sort of tiny peephole optimizer into it as gas macros, it occurred to me that (some) Forth systems are awfully close to being macro assemblers, and that really the only reason you’d use a higher-level language rather than a macro assembler is that error handling in macro assemblers, and in Forth, is terrible verging on nonexistent. Dynamically-typed languages give you high assurance that your program won’t crash (writing the Ur-Scheme compiler very rarely required me to debug generated machine code), while strongly-statically-typed languages give you similarly weak assurances with compile-time checks; but it seems clear that the programmer needs to be able to verify that their program is also free of bugs like memory leaks, infinite loops, SQL injection, XSS, and CSRF, or for that matter “billion-laughs”-like denial-of-service vulnerabilities, let alone more prosaic problems like the Flexcoin bankruptcy due to using a non-transactional data store. Against this background, we find that a huge fraction of our day-to-day software (X11, Firefox, Emacs, Apache, the kernel, and notoriously OpenSSL) is written in languages like C and C++ that lack even these rudimentary memory-safety properties, let alone safety against the trickier bogeymen mentioned above. The benefit of C++ is that it allows us to factor considerations like XSS and loops into finite, checkable modules; the benefit of C is that we can tell pretty much what the machine is going to do. But, as compiler optimizations exploit increasingly recondite properties of the programming language definition, we find ourselves having to program as if the compiler were our ex-wife’s or ex-husband’s divorce lawyer, lest it introduce security bugs into our kernels, as happened with FreeBSD a couple of years back with a function erroneously annotated as noreturn, and as is happening now with bounds checks depending on signed overflow behavior. We could characterize the first of these two approaches as “performing on the trapeze with a net”: successful execution is pleasant, if unexpected, but we expect that even a failure will not crash our program with a segfault — bankrupt Flexcoin, perhaps, and permit CSRF and XSS, but at least we don’t have to debug a core dump! The second approach involves performing without a net, and so the tricks attempted are necessarily less ambitious; we rely on compiler warnings and errors, careful program inspection, and testing to uncover any defects, with results such as Heartbleed, the Toyota accelerator failure, the THERAC-25 fatalities, the destruction of Ariane 5, and the Mars Pathfinder priority-inversion lockups. So onto this dismal scene sweep Kennedy, Benton, Jensen, and Dagand, with a novel new approach: rather than merely factoring our loops and HTML-escaping into algorithm templates and type conversion operators, thus giving us the opportunity to get them right once and for all (but no way to tell if we have done so), we can instead program in a language rich enough to express our correctness constraints, our compiler optimizations (§4.1), and the proofs of correctness of those optimizations. Instead of merely packaging up algorithms (which we believe to be correct after careful inspection) into libraries, we can package up correctness criteria and proof tactics into libraries. This is a really interesting and novel alternative to the with-a-net and the without-a-net approaches described earlier; it goes far beyond previous efforts to prove programs correct; rather than attempting to prove your program correct before you compile it, or looking for bugs in the object code emitted, it attempts, Forth-like, to replace the ecosystem of compi…

历次讨论

2014Hacker News 讨论帖187 分 · 61 评

HN 二十年，最值得读的论文。

朋友分享的书单

专题阅读路线

本周最多人读

我的书单

必读 30 篇

论文库

这些论文是怎么挑出来的

全量扫一遍

只留论文本身

写导读、译评论

Coq：世界上最好的宏汇编器？（2013）

导读

HN 评论精选

历次讨论

同领域还值得读

Google 的软件工程（2017）

Peter Naur：编程作为理论构建 (1985)

SciPy 1.0：Python 科学计算的基础算法

Lisp 的历史（1979）

使用 NumPy 进行数组编程

打赏支持

关注向阳乔木