Byron Cook，亞馬遜云科技自動(dòng)推理副總裁及杰出科學(xué)家

亞馬遜云科技是唯一一家如此大規(guī)模使用自動(dòng)推理的云提供商。隨著越來越多的人使用自動(dòng)推理工具，這讓我們?cè)谔嵘詣?dòng)推理工具的可用性和可擴(kuò)展性上更容易進(jìn)行大量的投入。我們發(fā)現(xiàn)自動(dòng)推理工具越易于使用，它們的功能就會(huì)變得越強(qiáng)大，同時(shí)自動(dòng)推理工具的采用率也會(huì)變得越高。我們?cè)侥茏C明云基礎(chǔ)設(shè)施的正確性，對(duì)于那些看重安全的客戶而言我們的云就越有吸引力。正如本文所述，通過自動(dòng)推理，我們不僅能夠提高安全性，還能更快地為客戶提供更高性能的代碼，并最終節(jié)省客戶的成本。

在亞馬遜云科技應(yīng)用自動(dòng)推理的10多年時(shí)間里，我們發(fā)現(xiàn)經(jīng)過驗(yàn)證的代碼通常比它所替代的未經(jīng)驗(yàn)證的代碼性能更好。

這主要是因?yàn)樵隍?yàn)證過程中我們所做的bug修復(fù)通常會(huì)提升代碼的運(yùn)行性能。自動(dòng)推理讓開發(fā)人員有信心去探索額外的優(yōu)化，進(jìn)一步提升系統(tǒng)性能。我們發(fā)現(xiàn)驗(yàn)證的代碼更容易更新、修改和操作，這減少了半夜的日志分析和調(diào)試環(huán)節(jié)。

自動(dòng)推理的基本概念

在亞馬遜云科技，我們努力為客戶構(gòu)建簡(jiǎn)單、易用的服務(wù)。但在這種簡(jiǎn)單的背后卻是龐大、復(fù)雜的分布式系統(tǒng)，每秒處理著數(shù)十億個(gè)請(qǐng)求。驗(yàn)證這些復(fù)雜系統(tǒng)的正確性是一個(gè)極大的挑戰(zhàn)。我們的服務(wù)隨著新功能的增加、組件的重新設(shè)計(jì)、安全的增強(qiáng)和性能的優(yōu)化，一直處于不斷變化和發(fā)展的狀態(tài)。很多變化本身就是非常復(fù)雜的，必須在不影響亞馬遜云科技本身或客戶的安全性和韌性的前提下進(jìn)行。

設(shè)計(jì)評(píng)審、代碼審計(jì)、壓力測(cè)試和故障注入是我們經(jīng)常以及未來都會(huì)一直使用的寶貴工具。然而，我們發(fā)現(xiàn)仍然需要使用額外的技術(shù)來確認(rèn)許多情況下的正確性。細(xì)微的bug仍可能逃過檢測(cè)，尤其是在大規(guī)模、容錯(cuò)架構(gòu)中。有些問題甚至可能源于最初的系統(tǒng)設(shè)計(jì)，而不是實(shí)施缺陷。隨著我們服務(wù)規(guī)模和復(fù)雜性的增長(zhǎng)，我們不得不使用基于數(shù)學(xué)和邏輯的更強(qiáng)大技術(shù)作為對(duì)傳統(tǒng)測(cè)試方法的補(bǔ)充。這就是人工智能(AI)的一個(gè)分支自動(dòng)推理發(fā)揮作用的地方。

傳統(tǒng)測(cè)試側(cè)重于在特定場(chǎng)景下驗(yàn)證系統(tǒng)行為，而自動(dòng)推理旨在使用邏輯來驗(yàn)證系統(tǒng)在任何可能場(chǎng)景下的行為。即使是一個(gè)中等復(fù)雜的系統(tǒng)，要重現(xiàn)可能發(fā)生的每一種可能狀態(tài)和參數(shù)的組合，所需的時(shí)間也是難以想象的。自動(dòng)推理可以通過計(jì)算系統(tǒng)正確性的邏輯證明來快速、高效地取得相同的效果。

使用自動(dòng)推理需要我們的開發(fā)者具有不同的思維方式。我們不是試圖考慮所有可能的輸入場(chǎng)景及其可能出錯(cuò)的方式，而是定義系統(tǒng)應(yīng)該如何工作，并識(shí)別出讓它正確運(yùn)行必須滿足的條件。然后，我們可以使用數(shù)學(xué)證明來驗(yàn)證這些條件是否為真。換句話說，我們可以驗(yàn)證系統(tǒng)是否正確。

自動(dòng)推理將系統(tǒng)的規(guī)范和實(shí)施以數(shù)學(xué)的形式進(jìn)行審核，然后使用算法來驗(yàn)證系統(tǒng)的數(shù)學(xué)表示是否滿足規(guī)范。通過把我們的系統(tǒng)編碼為數(shù)學(xué)系統(tǒng)，并使用形式邏輯對(duì)其進(jìn)行推理，自動(dòng)推理使我們能夠有效和權(quán)威地解答有關(guān)系統(tǒng)未來行為的關(guān)鍵問題。系統(tǒng)能做什么？它將做什么？它永遠(yuǎn)不會(huì)做什么？自動(dòng)推理可以幫助回答系統(tǒng)的這些問題，即便是最復(fù)雜的、大規(guī)模的和潛在無限的系統(tǒng)——這些場(chǎng)景是單單通過傳統(tǒng)測(cè)試無法徹底驗(yàn)證的。

自動(dòng)推理能讓我們達(dá)到完美的程度嗎？不能，因?yàn)樗匀灰蕾囉趯?duì)系統(tǒng)組件的正確行為以及系統(tǒng)與其環(huán)境模型之間關(guān)系的某些假設(shè)。例如，系統(tǒng)模型可能錯(cuò)誤地假設(shè)底層組件（如編譯器和處理器）沒有任何bug（盡管也可以對(duì)這些組件進(jìn)行驗(yàn)證）。話雖如此，與使用傳統(tǒng)軟件開發(fā)和測(cè)試方法相比，自動(dòng)推理讓我們更有信心達(dá)到正確性。

更快的開發(fā)

自動(dòng)推理不僅僅是數(shù)學(xué)家和科學(xué)家的工具。我們的 Amazon Simple Storage Service (Amazon S3) 工程師每天都在使用自動(dòng)推理來防止bug。S3的背后是世界上最大、最復(fù)雜的分布式系統(tǒng)之一，它存儲(chǔ)了400萬億個(gè)對(duì)象、EB級(jí)別的數(shù)據(jù)并通常需要每秒處理1.5億個(gè)請(qǐng)求。S3由許多子系統(tǒng)組成，這些子系統(tǒng)本身就是分布式系統(tǒng)，其中許多由數(shù)萬臺(tái)機(jī)器組成。S3一直不斷增加新的功能，同時(shí)它也被我們的客戶大量使用中。

S3索引子系統(tǒng)是S3的一個(gè)關(guān)鍵組件，它是一個(gè)對(duì)象元數(shù)據(jù)存儲(chǔ)，來支持快速的數(shù)據(jù)查找。該組件包含一個(gè)非常大的、復(fù)雜的數(shù)據(jù)結(jié)構(gòu)和精密的優(yōu)化算法。以S3的這種大規(guī)模，這些算法對(duì)于人類來說很難正確使用，同時(shí)我們也不能容許S3在查找時(shí)發(fā)生任何錯(cuò)誤，為此我們大約每個(gè)季度都會(huì)進(jìn)行新的改進(jìn)，但任何更改都是在極其謹(jǐn)慎和大量測(cè)試的前提下進(jìn)行的。

基于我們15年的經(jīng)驗(yàn)，S3是一個(gè)構(gòu)建良好以及經(jīng)過充分測(cè)試的系統(tǒng)。然而，我們?cè)欢葻o法確認(rèn)S3索引子系統(tǒng)中一個(gè)bug的根本原因。該系統(tǒng)能夠從異常中自動(dòng)恢復(fù)，因此該bug的存在并沒有影響系統(tǒng)的行為。但我們并不滿足于此。

為什么這個(gè)bug存在這么久？像S3這樣的分布式系統(tǒng)擁有大量組件，每個(gè)組件都有自己的異常情況（corner cases），而且有可能同時(shí)發(fā)生很多異常情況。就S3而言，它擁有超過300個(gè)微服務(wù)，這些異常情況的潛在組合的數(shù)量是巨大的。即使開發(fā)人員有證據(jù)證明bug存在，并可能知道引起bug的根本原因，但對(duì)于開發(fā)人員來說，他們不可能考慮到所有異常情況，更不用說這些異常情況的不同組合了。

這種復(fù)雜性促使我們探索如何使用自動(dòng)推理來探索可能隱藏在這些狀態(tài)中的可能狀態(tài)和錯(cuò)誤。通過構(gòu)建系統(tǒng)的正式規(guī)范，我們能夠找到bug并證明未來不存在此類bug。使用自動(dòng)推理也讓我們有信心每一兩個(gè)月發(fā)布一次更新和改進(jìn)，而不是一年只發(fā)布三或四次。

更快的代碼

Amazon Identity and Access Management (IAM)服務(wù)的正確性是確保我們客戶工作負(fù)載安全的基礎(chǔ)。每個(gè)發(fā)送到亞馬遜云科技的請(qǐng)求即每個(gè)API 調(diào)用都由IAM授權(quán)引擎處理，這會(huì)涉及到數(shù)百萬客戶、數(shù)千種資源類型和數(shù)百種亞馬遜云科技的服務(wù)。這種請(qǐng)求每秒就超過12億次。這是亞馬遜云科技中對(duì)安全要求最高以及需要高度擴(kuò)展的軟件之一。

在亞馬遜云科技，任何改變?cè)谶M(jìn)入到生產(chǎn)環(huán)境之前，我們需要有極高的信心確保系統(tǒng)保持安全和正確。使用自動(dòng)推理，我們可以證明我們的系統(tǒng)在幾乎所有情況下遵守特定的安全屬性。我們稱之為可證明的安全性。自動(dòng)推理不僅使我們能夠?yàn)榭蛻籼峁┛勺C明的安全保證，還讓我們能夠大規(guī)模交付功能、安全性和優(yōu)化。

與S3一樣，IAM在過去超過15年時(shí)間里，已經(jīng)成為一個(gè)經(jīng)過時(shí)間考驗(yàn)的、值得信賴的系統(tǒng)。但我們想進(jìn)一步提高標(biāo)準(zhǔn)。我們構(gòu)建了一個(gè)正式規(guī)范來捕獲現(xiàn)有IAM授權(quán)引擎的行為，將其策略評(píng)估原則編碼為可證明的定理，并使用自動(dòng)推理構(gòu)建了一個(gè)新的、更高效的實(shí)施。今年早些時(shí)候，我們部署了新的經(jīng)過證明正確的授權(quán)引擎——沒人注意到。自動(dòng)推理使我們能夠無縫地用經(jīng)證明正確的替換物代替授權(quán)引擎，一個(gè)最關(guān)鍵的亞馬遜云科技基礎(chǔ)設(shè)施之一。

有了規(guī)范和證明，我們可以很有信心的安全、積極地優(yōu)化代碼。在IAM的大規(guī)模下，每一微秒的性能改進(jìn)都意味著更好的客戶體驗(yàn)和我們自身更好的成本優(yōu)化。我們優(yōu)化了字符串匹配、刪除了不必要的內(nèi)存分配和冗余計(jì)算、加強(qiáng)了安全性并提高了可擴(kuò)展性。每次更新后，我們都會(huì)再次運(yùn)行證明，來確認(rèn)系統(tǒng)仍在正確運(yùn)行。

現(xiàn)在，優(yōu)化后的IAM授權(quán)引擎相比之前快了50%。如果不使用自動(dòng)推理，我們根本不可能這么有信心地進(jìn)行如此重要的優(yōu)化。

更快的代碼部署

大多數(shù)在線安全交易都受到加密保護(hù)。例如，RSA加密算法通過生成兩個(gè)密鑰來保護(hù)數(shù)據(jù)：一個(gè)用于加密數(shù)據(jù)，另一個(gè)用于解密數(shù)據(jù)。這些密鑰實(shí)現(xiàn)了安全的數(shù)據(jù)傳輸以及安全的數(shù)字簽名。在加密這種場(chǎng)景下，正確性和性能至關(guān)重要——加密算法中的一個(gè)bug可能是災(zāi)難性的。

隨著亞馬遜云科技客戶將工作負(fù)載遷移到Amazon Graviton上，針對(duì)ARM指令集的密碼優(yōu)化的好處也得到凸顯。但是，通過加密優(yōu)化獲得更好的性能是很復(fù)雜的，這使得驗(yàn)證修改后的加密算法是否正常運(yùn)行變得困難。在我們開始使用自動(dòng)推理之前，對(duì)密碼學(xué)庫進(jìn)行優(yōu)化通常需要數(shù)月的審查，才能獲得足夠的信心將其投入生產(chǎn)環(huán)境。

自動(dòng)推理的力量就在于此：正式驗(yàn)證使RSA更快，部署也更快。當(dāng)我們將自動(dòng)推理應(yīng)用于橢圓曲線密碼學(xué)時(shí)，我們也看到了類似的提升。

形成一個(gè)良性循環(huán)

我們?cè)谶^去十多年間，在亞馬遜云科技的內(nèi)部越來越多的應(yīng)用自動(dòng)推理技術(shù)來證明我們的云基礎(chǔ)設(shè)施和服務(wù)的正確性。我們經(jīng)常使用這些方法不僅用于驗(yàn)證正確性，而且還用于增強(qiáng)安全性和可靠性，以及最小化設(shè)計(jì)缺陷?？梢允褂米詣?dòng)推理為一個(gè)系統(tǒng)創(chuàng)建一個(gè)精確且可測(cè)試的模型，使用該模型快速驗(yàn)證更改是否安全，或者發(fā)現(xiàn)它們是不安全的來避免對(duì)生產(chǎn)環(huán)節(jié)產(chǎn)生有害影響。

我們可以回答關(guān)于我們基礎(chǔ)設(shè)施的一些關(guān)鍵問題，來檢測(cè)可能導(dǎo)致數(shù)據(jù)泄露的錯(cuò)誤配置。我們可以阻止一些我們無法通過其他技術(shù)發(fā)現(xiàn)的微妙但嚴(yán)重的錯(cuò)誤進(jìn)入生產(chǎn)環(huán)境。有了模型檢查，我們獲得了顯著的性能優(yōu)化，這是我們以往不敢嘗試的。自動(dòng)推理為關(guān)鍵系統(tǒng)按預(yù)期運(yùn)行提供了嚴(yán)格的數(shù)學(xué)保證。

亞馬遜云科技是唯一一家如此大規(guī)模使用自動(dòng)推理的云提供商。隨著越來越多的人使用自動(dòng)推理工具，這讓我們?cè)谔嵘詣?dòng)推理工具的可用性和可擴(kuò)展性上更容易進(jìn)行大量的投入。我們發(fā)現(xiàn)自動(dòng)推理工具越易于使用，它們的功能就會(huì)變得越強(qiáng)大，同時(shí)自動(dòng)推理工具的采用率也會(huì)變得越高。我們?cè)侥茏C明云基礎(chǔ)設(shè)施的正確性，對(duì)于那些看重安全的客戶而言我們的云就越有吸引力。正如前文所述，我們不僅能夠提高安全性，還能更快地為客戶提供更高性能的代碼，并最終節(jié)約客戶的成本。

我們正處于一個(gè)新時(shí)代的開端，在這個(gè)時(shí)代大規(guī)模云架構(gòu)的關(guān)鍵屬性，諸如安全、合規(guī)性、可用性、持久性和防護(hù)等都可以實(shí)現(xiàn)自動(dòng)證明。亞馬遜與眾不同之處就在于，我們從基礎(chǔ)就用可靠的數(shù)學(xué)推理并持續(xù)分析我們所構(gòu)建的一切，防止從AI幻覺到分析虛擬機(jī)監(jiān)控程序、密碼學(xué)和分布式系統(tǒng)等潛在問題的發(fā)生。