2.21 类型系统与静态分析

Overview and motivation

大多数缺陷都被发现得很晚（）在运行时，由一次测试、一位用户或一起事件发现。而有一整类缺陷根本不需要拖到那么晚。类型系统和优秀的静态程序分析工具会在代码运行之前读取它，并证明某些错误不可能发生：把字符串用在需要数字的地方、解引用了空值、变量在赋值前被读取、某个分支没有处理。本章讲的是把正确性推向左侧，推近到你写下这一行代码的那一刻（）此时修复只需几秒钟，而不是一整页事件复盘报告。

静态分析是指在不执行代码的情况下检查源代码或编译后代码的任何技术。类型检查是其中最普遍的形式，但这一大家族还包括代码检查工具（linter，用来标记风格和正确性方面的模式）、数据流分析器，以及处于最深处的形式化验证。这些工具共同的承诺是：每次构建都能免费获得一类保证，永远如此，不用写测试，也不用靠评审者记住。正是这个承诺，使这门学科与编码标准（第 2.1 章）、软件设计原则（第 2.2 章）和测试策略（第 2.4 章）并列：它是让大型代码库能够安全变更的又一种自动化手段。

对大型团队而言，这种价值会不断复合。当成百上千名工程师共同触碰一个共享系统时，类型签名就是编译器对每个人都强制执行的一份契约，流水线中的检查工具就是一位从不疲倦、从不偏袒的评审员。在企业场景中，这能降低新人上手和系统集成的成本，因为类型记录了意图，分析工具则能捕获新人常犯的错误。在政府及其他高风险系统中，一个错误的答案可能会导致某项福利被拒或数据泄露，机器检查过的保证就是证据：它向审计人员表明，整类故障从构造上就是不可能发生的，而不仅仅是未经测试。这与软件质量（第 2.11 章）和应用安全（第 4.2 章）直接相关。

Key principles

把正确性推向左侧：在编写代码时就捕获错误，而不是在生产环境中。
优先选择机器检查的保证，而不是依赖人类必须记住的约定。
把意图编码进类型中，使非法状态根本无法被表示。
在动态代码中逐步引入类型；不必一步到位。
把警告当作错误处理，并棘轮式收紧基线，使其只能变好。
在编辑器和流水线中运行相同的分析工具，使用完全相同的规则。
用有纪律、有理由、可审查的方式来管理误报的抑制（suppression）。

Recommendations

Choose static or dynamic typing with eyes open

在静态类型语言中，类型在程序运行之前就被检查；在动态类型语言中，类型是在运行时才被检查的（如果有检查的话）。二者并非哪个绝对正确，诚实的说法是：这是在保证与灵活性之间做权衡。静态类型为你换来机器检查的契约、可信赖的重构，以及了解事物具体类型的工具支持（自动补全、安全重命名、跳转到定义）。动态类型为你换来快速原型开发、简洁的代码，以及适合脚本和探索性工作的低仪式感。系统越大、生命周期越长、风险越高，静态一方的回报就越大，因为全代码库重构的成本和运行时类型错误的成本都会随规模增长。

还要区分另一条正交的轴线：强类型与弱类型。强类型语言拒绝悄悄地在不兼容类型之间做隐式转换（把数字加到字符串上会报错）；弱类型语言则会悄悄转换，产生诸如 "3" + 4 得到你意想不到的结果这类意外。你可以拥有”静态且弱类型”或”动态且强类型”的组合。评估一门语言时，要把这两个问题分开来问，因为人们说”有类型”时，实际想要的往往是”强类型”。

Lean on type inference to keep types cheap

对静态类型的一个常见反对意见是：每一行都要写类型太啰嗦。类型推断消除了这部分成本的大头：编译器根据上下文推导出类型，因此你只需要在边界处（函数签名、公共接口）标注类型，内部则交给推断。现代语言的推断能力很强，让你既能获得静态检查的安全性，又能享有接近动态代码的简洁性。可以定一条团队规则：为读者依赖的契约部分（导出的函数和公共类型）标注类型，而把局部变量留给推断。这样既能让签名保持诚实、自解释，又能让内部代码免于杂乱，也呼应了第 2.1 章关于可读性的目标。

Make illegal states unrepresentable

在实践中的类型设计里，最强大的理念是：让你的类型在结构上就无法写出错误的状态。如果一个订单要么是没有付款的”草稿”，要么是已付款的”已下单”，就不要把它建模成一个带有可空字段的结构体，让草稿可能意外携带付款信息、已下单状态却可能没有付款信息。而应把它建模为和类型（也叫标签联合、可辨识联合或变体）：一个值恰好是固定集合中某一种形状，每种形状携带各自的数据。这样一来，非法组合根本不存在，处理该值的代码必须覆盖每一种情形，否则编译器就会报错。这把运行时的”本不应该发生”变成了编译期的”不可能发生”，而这正是问题的关键所在。

同样的直觉也驱动着许多日常工具。对于一组固定的状态，使用枚举类型而不是魔法字符串。把经过校验的值包装成一个独立的类型（比如用 EmailAddress 而不是裸字符串），这样”未校验的输入”和”已校验的邮箱地址”就是编译器能够区分开的不同类型。这正是错误处理（第 2.20 章）中边界校验原则在类型系统层面的体现：在边界处只校验一次，转换成一个编码了保证的类型，让内部代码信任它。

Take nullability and generics seriously

空指针（）其发明者称之为自己”十亿美元的错误”（）曾经是静态类型系统最常见的撒谎方式：一个被标注为字符串类型的值，可能悄悄是空的，而你往往是在程序崩溃时才发现这一点。现代类型系统通过让可空性显式化来解决这个问题。一个值要么是永远不为空的 String，要么是必须在使用前解包的 Option/Maybe/可空类型，编译器会强制你处理空值的情形。如果你的语言提供了非空类型或可选类型，就在所有地方使用它们，并把裸露的可空类型当作一种代码异味（smell）。这样就能消除整整一类生产环境的崩溃。

泛型，也叫参数多态，让你能编写适用于多种类型的代码，同时不放弃类型安全：List<T> 是某个具体类型 T 的列表，在编译期就会被检查，而不是一堆未类型化、需要靠强制转换和祈祷来处理的东西。构建可复用的容器、函数和抽象时，应善用泛型来保持强类型。和类型、非空类型与泛型三者的组合，正是让现代类型系统能够表达真实领域规则、而不只是给原始类型贴标签的关键所在。

Adopt types gradually in existing dynamic code

你不必重写整个动态代码库就能获得类型带来的好处。渐进式类型让有类型代码和无类型代码共存，因此你可以在收益最大的地方逐步添加类型。如今许多生态系统都直接支持这种方式：Python 中由独立类型检查器检查的类型提示、编译到动态语言的有类型超集，或是叠加在现有运行时之上的类型注解。从边界和最关键的模块（涉及资金的代码、安全相关代码、数据模型）开始，先以宽松模式开启检查器，再随时间逐步收紧。再加一条规则：即便旧代码尚在追赶进度，新代码也必须有类型。几个季度之内，一个庞大的无类型代码库就能达到大多数改动都经过类型检查的程度，而最重要的部分会最先被覆盖。

Run linters, type checkers, and deeper analysers together

类型检查只是一层，还要加上其他层。代码检查工具（lint）能捕获类型检查器忽略的可疑模式：恒为真的赋值、未使用的变量、switch 语句中的贯穿（fall-through）、从未关闭的资源。更深层的分析工具会推理程序的行为。数据流分析追踪值在代码中的流动，以回答诸如”这个变量是否在赋值前就被使用了”或”这条错误路径上是否会发生文件句柄泄漏”之类的问题。这些工具中有许多建立在抽象解释之上，这是一种在可能取值的集合（例如”正数""零”或”负数”，而不是具体数字）上抽象地运行程序的技术，用以一次性证明所有执行路径都满足某种性质，而无需真正运行任何一条路径。

有些分析工具与安全工具相邻。静态应用安全测试（SAST）扫描源代码，寻找注入、不安全的反序列化，或受污染数据流向危险汇点等漏洞模式，它与本节所述的数据流机制共享底层技术；把它视为这一大家族的一员，并与应用安全（第 4.2 章）协同起来。实践建议是采用分层组合：一个用于风格和明显错误的快速代码检查工具、一个用于契约的类型检查器，以及一个或多个针对你所在领域重要属性的深层分析工具。把它们的配置放在版本控制的文件中，确保每个人使用的规则完全一致。

Treat warnings as errors and ratchet the baseline

一个不会让构建失败的警告，就是一个会被忽略的警告。一旦日志中堆满成百上千条被容忍的警告，就没有人会去读它，真正重要的那一条就会淹没在噪音中。采用”把警告当作错误”的策略，使新出现的警告会中断构建，并在修复成本最低的那一刻就被修复。对于已有成千上万条警告的遗留代码库，你无法一夜之间切换这个开关，因此要使用棘轮机制：把当前数量记录为基线，阻止任何会使该数量增加的改动，并随时间将其逐步降低。基线只能下降，不能上升。这让你能够今天就启用一条严格规则，而不需要先做一次大规模的前期清理，同时保证情况永远不会变得更糟，并稳步变好。

Wire analysis into editors and CI, with fast feedback

静态分析在反馈即时的情况下收益最大。通过语言服务器协议或同等机制，在编辑器中运行同一套检查，让开发者在输入代码的过程中（）甚至在保存之前（）就能看到错误。然后在持续集成（CI）中运行完全相同的规则集，确保没有任何改动能在未通过检查的情况下合并，这与第 8.1 章的流水线相衔接。二者必须保持一致：如果编辑器宽松而 CI 严格，或者反过来，人们就会对两者都失去信任。要让分析足够快，能在每次改动时都运行，缓存结果，并尽可能只分析发生变化的部分，这样检查工具才是助力而非负担。当编辑器和流水线以相同的方式强制执行相同的规则时，标准就不再是一份被人遗忘的文档，而成为环境本身的一种属性。

Reserve formal verification for the code that warrants it

在这个光谱的最深处是形式化验证：用数学方法证明程序满足某个精确的规约，而不仅仅是通过了测试。相关技术从模型检验（穷举探索系统的所有状态）到定理证明，再到依赖类型（表达能力足以编码完整规约的类型）不等。这是目前可获得的最深层保证，也是成本最高的一种，因此只有在缺陷会造成灾难性后果，或认证要求如此的场合才值得投入：加密库、飞行控制代码、虚拟机监控程序（hypervisor）、关键协议。对大多数软件而言，正确的投入是强类型加上优质的分析工具，它们能以远低得多的成本捕获大部分收益。要知道形式化方法（在第 2.12 章中介绍）的存在及其适用边界，这样你才能在极少数确实需要它的组件上有意识地动用它。

Keep suppression honest

没有一个分析工具是完美的，而区分”被信任的工具”和”被忽视的工具”的关键，在于你如何处理它的失误。每一个正经的工具都允许你抑制某个发现（finding）。要求每一次抑制都必须范围狭窄（针对一行代码或一个发现，而不是整个文件或整条规则）、在注释中说明理由，并且和其他代码一样在评审中可见。在文件顶部一次性全面禁用，正是覆盖率悄悄腐坏的方式。定期审计抑制记录，把数量不断增长的抑制视为一个信号：要么是某条规则校准有误，要么是代码中确实存在某个被人藏起来的真实问题。诚实的抑制让工具保持可信；沉默、大范围的抑制则会把它变成一场表演。

Trade-offs: pros and cons

Approach	Pros	Cons
静态类型	机器检查的契约；安全的重构；丰富的工具支持	前期仪式感更强；早期原型开发更慢
动态类型	编写速度快；灵活；仪式感低	类型错误在运行时才暴露；重构有风险
类型推断	兼具安全性与简洁性；注解噪音更少	过度使用时，推断出的类型可能掩盖意图
渐进式类型	可增量采用；优先覆盖关键代码	未类型化的边缘仍会泄漏问题；保证是部分的
代码检查工具与数据流分析	能捕获类型系统遗漏的错误；运行成本低	存在误报；未配置好时噪音较多
警告即错误 + 棘轮机制	新问题会被阻断；基线只会变好	可能让人感觉受阻；需要配套的抑制策略
形式化验证	保证最强；能对所有输入证明性质	成本高、需要专业能力；很少能被证明合理

反复出现的张力是保证与摩擦之间的权衡。类型越严格、分析越深入,你就能让越多一类错误变得不可能发生,同时也会增加仪式感、工具运行时间,偶尔还会有让开发者浪费几分钟的误报。要根据风险和生命周期来权衡:一次性脚本或原型探索想要的是轻量、快速的动态一端。而一个支付账本、一项权限校验,或者一个政府将运行十五年的系统,则需要强类型、分层的分析工具、警告即错误,以及（）对其中最危险的核心部分（）或许还需要形式化证明。让严格程度与出错代价相匹配,并借助类型推断和渐进式采用来保持摩擦在可承受范围内。

Questions to discuss with your team

我们代码库中的哪些地方,类型系统本可以阻止我们最近的几起生产事件,我们知道吗? 大多数团队都在抽象地争论类型系统,而证据其实就摆在他们自己的事件历史中。翻出最近十到二十个生产缺陷并加以归类:有多少是本应有值却出现了 null、跨边界传递的形状不对、某个分支未被处理、某个字符串类型的值悄悄”漂移”了含义?这些正是类型检查器和代码检查工具能够免费捕获的错误。如果你的事件中有很大比例落在这个类别里,那么在这些事件发生的模块中加强类型就有了具体的、可以用金钱衡量的理由。如果几乎没有,那么你的缺陷存在于别处(逻辑、并发、需求),更重的类型投入可能不是你当前价值最高的举措。无论哪种情况,你都用数据取代了主观意见。
如果我们采用渐进式类型,应该从哪里开始,“足够完成”意味着什么? 在一个庞大的动态代码库中打开检查器是一个持续推进的计划,而不是拨一下开关那么简单,排序方式决定了它是成功还是停滞。讨论哪些模块承担着最大的风险(资金、鉴权、核心数据模型),因此应优先获得类型,而哪些模块足够稳定、风险足够低,可以暂时保持无类型。为新代码定下一条规则(从第一天起就要有类型),这样在你逐步清理存量代码的同时,无类型的面积不再继续扩大。定义一个目标:也许是每一个公开函数签名都有类型、每一个边界都被校验转换为某个类型、检查器在关键包上以严格模式运行。没有明确的终点线,渐进式类型就会变成永无止境、只覆盖了一半的状态,这是两头都不讨好的结果。
当静态分析工具出错时,我们的策略是什么,这套策略能否保持工具的可信度? 每个分析工具都会产生误报,而你如何处理它们,决定了这个工具最终是保持有用,还是在挫败中被人弃用。逐一讨论具体案例:当某个发现确实是误报时,抑制是否范围狭窄、在注释中说明了理由,并在评审中可见,还是有人直接为整个代码库禁用了整条规则?看看你现在的抑制记录:一共有多少条,是否都写明了理由,上一次有人审计它们是什么时候?一堆没有说明理由、范围宽泛的抑制,意味着你的覆盖率其实是空心的。目标是建立一套共享的、被强制执行的纪律,让分析工具的发现真正被信任并被采纳行动,而不是被条件反射式地噤声。
我们在语言和分析工具上应该统一到什么标准,当技术栈在各团队之间分裂时,我们如何保持一套规则? 当成百上千名工程师使用多种语言工作时,每个团队各自漂移到自己的检查工具、自己的代码检查规则、自己的严格程度设置,都会悄悄摧毁这份保证,因为在一个仓库中被强制执行的契约,到了下一个仓库可能只是一条建议。这种拉扯是真实存在的:中央统一化能带来工程师的可流动性和一致的审计证据,但从中心强加的规则集也可能与某种语言的惯用法相冲突,或拖慢一个原本有充分理由采用自己配置的团队。把生产环境中使用的语言清单、每个团队运行的分析工具及其版本,以及它们规则集之间的差异带到讨论中来,让这种分化变得可见,而不是被想当然地忽视。在企业或政府场景中,把答案与采购和审计挂钩:一份每个仓库都继承的、版本受控的统一配置,才能让审计人员确认所有地方运行的是同一套检查,也才能阻止供应商在比你自己员工所遵守的规则更宽松的条件下交付代码。
我们的分析速度有多快,人们会在什么时候开始绕开它? 检查工具只有在每次改动时都运行,才称得上是一种保证,而一旦它让编辑，构建循环变得痛苦,工程师就会学会跳过它、在本地禁用它,或者带着红色的检查结果合并代码,并许诺”以后再修”。这里的张力是深度与速度之间的权衡:更深层的数据流或安全分析能发现快速代码检查工具遗漏的错误,但如果完整套件要跑二十分钟,人们就会停止等待,而没有人愿意等待的检查等于没有保护任何东西。把真实数字带到讨论中来:编辑器反馈延迟、分析阶段在 CI 中的实际耗时、缓存命中率、构建在检查被跳过或被覆盖的情况下合并的频率,以及运行中有多少是增量分析、多少是全量分析。对于大型或面向公众的组织,还要加上计算成本和吞吐量成本,因为在整个机群的规模下,一个缓慢的强制性分析阶段既是预算上的一笔开支,也是拖慢每一次发布的一条队列,而诚实的解决办法通常是增量分析和缓存,而不是悄悄放宽规则。
我们究竟能为审计人员提供哪些机器检查过的证据,它覆盖了我们哪些关键的不变量? 在受监管和高风险的系统中,类型系统和静态分析的意义在于:除了日常预防的那些缺陷之外,还能提供可证明的证据,表明整类故障从构造上就是不可能发生的（）而如果你无法说明具体强制执行了哪些不变量、覆盖到了哪里,这个主张就是空谈。这里的权衡是范围与成本的对立:证明得越多(处处非空、每一种合法状态都用和类型表达、对核心计算做形式化验证),换来的证据就越强,但每向严格程度上迈一步,都要付出注解工作量、专家时间和构建复杂度的代价,而这些在低风险代码上未必值得。带上一份地图,列出你的安全关键模块目前各自具备哪些保证、附带理由的未结抑制清单,以及任何一个关键规则仅靠约定而非编译器强制执行的缺口。对于政府或受监管的企业,把这个问题定位成认证证据:审计人员应当能够把一项必需的属性追溯到某个机器检查过的类型或证明,并看到记录每一项例外的抑制日志,这样合规就建立在工具链生成的工件之上,而不是事后的人工评审。

Sector lens

Startup. 速度制胜,因此要选择成本最低、又不会拖慢你的安全手段:一门强类型语言,或以宽松模式运行的类型检查器,再加上编辑器中的快速代码检查工具,并优先为涉及资金和鉴权的代码添加类型。完全跳过形式化验证和深层数据流分析套件,它们耗费的时间是你负担不起的。你早期想要的回报,是在代码量达到一万行时仍能放心地重构,所以要在代码库变得难以驾驭之前就打开检查器。

Small business. 由于没有静态分析专职人员,应优先选择内置良好默认设置的语言和工具链,而不是一套需要自己调优和照看的套件。把分析能力嵌入到你的 IDE 和托管 CI 中直接使用,而不是自己搭建平台,并让规则集贴近社区标准,这样承包商或新员工也能一眼认出来。把”警告即错误”和一个小而精的类型化核心,当作你有限预算下杠杆效应最高的举措。

Enterprise. 这里的工作是跨众多团队的治理:一份每个仓库都继承的、版本受控的配置,编辑器和流水线中完全相同的规则,以及一条棘轮式收紧的基线,确保任何团队的覆盖率都不会悄悄下滑。统一分析工具,把类型覆盖率和抑制数量作为组合层面的指标来追踪,并按固定节奏审计抑制记录,使机器检查的保证在整个组织中保持一致,足以让审计人员信赖。为拥有这份共享配置的平台团队编列预算,因为在数千名工程师之间维持一致性不会自动发生。

Government. 采购、透明度和长生命周期在这里占主导地位。在合同中要求供应商遵守与你自己员工相同的分析规则,并把配置和抑制日志作为交付物移交,这样即便更换供应商,这份保证也能延续下去。在资格审核和支付逻辑上,优先选择机器检查的证据而不是人工保证,把形式化验证留给那些一旦失败就会非法剥夺某项福利的计算,并在系统运行的十年甚至更长时间里,让每一次抑制都留有据可查的记录。

Examples

Startup. 一家六人的初创公司为求速度,用一门动态语言构建产品,这在代码量达到一万行之前一直表现良好,直到一次重构开始在生产环境中引发运行时类型错误,而他们只能在生产环境中才发现这些错误。他们采用了渐进式类型:以宽松模式开启类型检查器,先为核心领域模型和支付代码添加类型提示,并制定规则,要求所有新模块必须完全类型化。他们用相同的配置把检查器和代码检查工具接入编辑器和 CI,把新出现的警告当作错误,同时棘轮式收紧已有的警告。两个季度之内,因形状不匹配导致的崩溃消失了,重构不再令人畏惧,新员工的自动补全也真正知道每个函数返回的是什么。这项投入花费了几个工程师-周,却消除了一个反复出现的、影响客户的缺陷来源。

Enterprise. 一家全球性银行在数千名工程师之间统一了静态分析。每个仓库都继承一份共享配置:严格模式下的类型检查器、代码检查工具、数据流分析器,以及用于安全模式的 SAST 扫描器,全部在编辑器中运行,并在流水线中强制执行,确保没有任何改动能在未通过检查的情况下合并。领域类型使得涉及资金流转的代码中,非法状态根本无法表示:已入账的交易和待处理的交易是不同的类型,货币被类型化,使你无法把美元和欧元相加,经过校验的输入与原始输入是不同的类型。警告即错误,每个团队的基线都只能下降。抑制必须附带理由,并按季度审计。由于这些保证是机器检查、全组织一致的,审计人员能够确认整类故障从构造上就是不可能的,工程师们也能放心地在不熟悉的服务之间穿梭工作。

Government. 某国家税务机关正在对一套福利计算系统进行现代化改造,该系统必须在多年内保持正确且可解释。核心的资格认定逻辑用一门强类型语言编写,领域模型将规则本身编码在其中:申请人的状态是一个覆盖每一种合法情形的和类型,金额是一个专用类型,不会与计数值混淆,任何可能缺失的值都不会被留作裸露的可空类型。静态分析在 CI 中作为一道关卡运行,而最安全攸关的计算模块还额外使用形式化方法进行检查,以证明关键不变量对所有输入都成立,从而满足认证要求。每一次抑制都留有据可查的记录。当最初的作者离职后,继任者们接手的是一份契约由编译器强制执行的代码,因此十年之后他们依然可以安全地修改它。

Business case: motivations, ROI, and TCO

类型系统和静态分析带来的回报,本质上是缺陷成本发生地的一次转移。一个在编辑器中被类型检查器捕获的错误,成本只有几秒钟;同一个错误如果在生产环境中被发现,成本则是一起事件、一次调查,可能还有客户损害和监管处罚。关于缺陷经济学的研究一致表明,一个缺陷每多存活一个阶段（）从编写到评审到测试再到生产（）其成本就会上一个数量级。静态分析把整整一类缺陷转移到了成本最低的那个阶段,且每次构建都如此,不需要按缺陷计费的人力投入。这是一笔固定的、大多是一次性的建设成本,换来的却是源源不断被预防的缺陷流,这在工程学中已经接近于最佳的杠杆效应。

成本是真实存在的,但规模适中且前置。你需要选择并配置工具,在注解上付出一些仪式性成本(可通过类型推断缓解),花工程师的时间在遗留代码中采用渐进式类型,并接受偶尔出现的误报。与之相对,要权衡另一种选择的总拥有成本:每一个因类型问题而流入生产环境的缺陷、每一次因为没有任何东西能保证正确性而回避掉的高风险重构、每一次因为代码没有自我记录契约而拖慢的新人上手过程,以及在受监管场景中,每一次不得不靠人工评审而非机器检查证据来满足的审计。要向管理层证明这一点,应把它与他们已经在追踪的指标挂钩:变更失败率、缺陷逃逸率、平均恢复时间,以及可归因于本可预防的类型错误和空值错误的事件占比。真正能说服人的图表,是按”检查工具本可捕获与否”排序的你自己的事件历史。

Anti-patterns and pitfalls

把逃生舱口当习惯: 把值强制转换为 any、dynamic 或等价的无类型形式来让检查器闭嘴,恰恰在你最需要保证的地方抹去了它。
一切都是字符串类型: 在跨边界传递时使用裸字符串和无类型的映射,而不是把状态建模为真正的类型,导致编译器无法提供任何帮助。
默认可空: 在语言已提供非空类型和可选类型的情况下,仍让值保持可空,延续着那个”十亿美元的错误”。
永远不会失败的警告: 成千上万条被容忍的警告中,真正重要的那一条彻底隐形,因为从来没有什么东西会真的导致构建失败。
编辑器与 CI 不一致: 本地宽松而流水线严格,或者反过来,导致开发者对两者都失去信任,合并结果也让人感到意外。
一刀切的抑制: 禁用整条规则或整个文件,而不是针对一个有理有据的发现,悄悄掏空了覆盖率。
分析表演: 运行一堆没有人阅读或采纳的分析工具,报告不断堆积,价值却是零。
全有或全无的类型化: 因为无法一次性给所有代码加上类型就拒绝开始,从而放弃了优先为关键代码加上类型所能带来的巨大收益。
到处都用形式化验证: 在普通代码上动用形式化方法,把稀缺的专家精力花在本来强类型就足够的地方。

Maturity model

Level 1, Initiate: 类型化和分析是随意的、因人而异的。动态代码没有检查器,或者静态语言虽然运行着检查却对警告置之不理。类型相关的缺陷(空值、形状不对、未处理的分支)频繁流入生产环境,重构令人畏惧,因为没有任何东西能验证正确性。
Level 2, Develop: 部分项目上运行着代码检查工具,在相关的地方也运行着类型检查器,但规则在各团队之间不一致,警告不会导致构建失败,逃生舱口和大范围抑制很常见。已经产生了一些收益,但覆盖率参差不齐,对工具的信任也时好时坏。
Level 3, Standardize: 一份共享的、版本受控的配置,在编辑器和 CI 中以完全相同的规则强制执行类型检查和代码检查。警告即错误,基线棘轮式收紧,在边界处使用可空性和和类型使非法状态无法表示,每一次抑制都需要有据可查、可供评审的理由。
Level 4, Manage: 分析工作被度量并对照基线加以管控。关键模块的类型覆盖率、警告数量、误报率、抑制数量,以及检查器本可捕获的生产事件占比,都被对照明确的目标持续追踪。这些指标会反过来约束变更:资金和鉴权代码的覆盖率不能下降,误报率上升会触发规则重新校准,仪表盘显示的是这些保证是否真正生效,而不只是配置得看起来生效。
Level 5, Orchestrate: 分析工作在整个组织范围内持续改进和整合。渐进式类型已覆盖到关键模块,数据流和安全分析器例行运行,规则随语言和威胁的演变而调整,形式化验证被有意识地应用于那少数一旦失败就会造成灾难性后果的组件。工具、指标和规则集反过来又反馈进设计、招聘和采购之中,使整个组织在变更面前变得越来越稳妥安全。

Ideas for discussion

你最近的哪些生产缺陷本可以被类型检查器或代码检查工具捕获,它们占总数的比例是多少?
在你的领域模型中,哪里可以用和类型或经校验的包装类型,把运行时的”本不应该发生”变成编译期的”不可能发生”?
如果你明天就把警告变成错误,会有多少条导致构建失败,需要什么样的基线和棘轮机制,才能让你在不发起一场清理运动的情况下采用这项政策?
你的编辑器和流水线运行的是完全相同的规则吗?开发者要如何发现两者是否已经出现分歧?
你的代码库中现在存在多少条抑制记录,其中有多少附带了理由,上一次审计是什么时候?
你的系统中是否存在某个组件,其失败后果严重到足以证明形式化验证是值得的?你又是如何判断的?

Key takeaways

静态类型和分析把整整一类缺陷推向了修复成本最低的那一刻:在你编写代码、每次构建的时候,而且不需要按缺陷计费的人力投入。
优先选择机器检查的保证,而不是依赖人类必须记住的约定,把意图编码进类型中,使非法状态根本无法被表示。
你不必一步到位:渐进式类型让你可以优先覆盖关键代码(资金、鉴权、数据模型),其余部分随后跟上。
把警告当作错误,搭配棘轮式收紧的基线,在编辑器和 CI 中运行完全相同的规则,并让抑制保持范围狭窄、有理有据、可供审计。
让严格程度与风险相匹配:对大多数系统而言,强类型加分层分析工具就足够,形式化验证则留给那少数一旦失败就是灾难性后果的组件。

References and further reading

Benjamin C. Pierce, Types and Programming Languages
Simon Peyton Jones (ed.), The Implementation of Functional Programming Languages
Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis
Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”
Scott Wlaschin, Domain Modeling Made Functional
Steve McConnell, Code Complete: A Practical Handbook of Software Construction
Michael Barr and the MISRA Consortium, MISRA C: Guidelines for the Use of the C Language in Critical Systems
Al Bessey et al., “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World,” Communications of the ACM