大規(guī)模應(yīng)用自動(dòng)推理提升系統(tǒng)效率

01

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

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

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

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

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

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

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

02

更快地開(kāi)發(fā)

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

Amazon S3索引子系統(tǒng)是Amazon S3的一個(gè)關(guān)鍵組件，它是一個(gè)對(duì)象元數(shù)據(jù)存儲(chǔ)，支持快速查找數(shù)據(jù)。該組件包含一個(gè)龐雜的數(shù)據(jù)結(jié)構(gòu)和精密的優(yōu)化算法。這些算法對(duì)于開(kāi)發(fā)者來(lái)說(shuō)很難被精準(zhǔn)掌握，并且Amazon S3在查找時(shí)不能被容許發(fā)生任何錯(cuò)誤，為此亞馬遜云科技大約每個(gè)季度都會(huì)在極其謹(jǐn)慎和大量測(cè)試的前提下進(jìn)行新的改進(jìn)。

憑借亞馬遜云科技15年的經(jīng)驗(yàn)積淀，Amazon S3已發(fā)展成為一個(gè)穩(wěn)健且經(jīng)過(guò)嚴(yán)格測(cè)試的系統(tǒng)。然而，在Amazon S3索引子系統(tǒng)中曾出現(xiàn)一個(gè)難以追溯根源的bug，雖然系統(tǒng)具備自動(dòng)異?；謴?fù)能力，讓這個(gè)bug無(wú)法對(duì)整體系統(tǒng)造成影響，但它的存在并不能讓一直追求更高穩(wěn)定性和可靠性的亞馬遜云科技開(kāi)發(fā)人員滿足。

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

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

03

更快的代碼

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

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

與Amazon S3一樣，Amazon IAM在過(guò)去超過(guò)15年時(shí)間里，已經(jīng)成為一個(gè)經(jīng)過(guò)時(shí)間考驗(yàn)的、值得信賴的系統(tǒng)。但亞馬遜云科技想進(jìn)一步提高標(biāo)準(zhǔn)，通過(guò)構(gòu)建一個(gè)正式規(guī)范來(lái)捕獲現(xiàn)有Amazon IAM授權(quán)引擎的行為，將其策略評(píng)估原則編碼為可證明的規(guī)范，并使用自動(dòng)推理實(shí)現(xiàn)更高效的實(shí)施。今年早些時(shí)候，通過(guò)使用自動(dòng)推理工具，亞馬遜云科技得以成功將原有授權(quán)引擎無(wú)縫替換并高效實(shí)施。

依托于規(guī)范和證明的支持，亞馬遜云科技能夠更有信心地安全優(yōu)化代碼。由于Amazon IAM的廣泛應(yīng)用，每一微秒的性能改進(jìn)都意味著更好的客戶體驗(yàn)和更好的成本優(yōu)化。通過(guò)優(yōu)化字符串匹配、刪除不必要的內(nèi)存分配和冗余計(jì)算，加強(qiáng)Amazon IAM的安全性并提高可擴(kuò)展性。每次更新之后，開(kāi)發(fā)團(tuán)隊(duì)都會(huì)重新運(yùn)行證明，以確保系統(tǒng)繼續(xù)按照預(yù)期運(yùn)行。

如今，優(yōu)化后的Amazon IAM授權(quán)引擎相比之前提速50%。自動(dòng)推理不僅提高了性能，還極大增強(qiáng)了亞馬遜云科技開(kāi)發(fā)團(tuán)隊(duì)對(duì)系統(tǒng)穩(wěn)定性的信心。

04

更快部署代碼

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

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

通過(guò)使用自動(dòng)推理進(jìn)行正式驗(yàn)證，不僅加速了RSA算法的運(yùn)行效率，也加快了其部署速度；并且將這種應(yīng)用于橢圓曲線密碼學(xué)（一種加密技術(shù)）時(shí)，還能顯著提升性能。

05

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

在過(guò)去十余年的時(shí)間里，亞馬遜云科技積極應(yīng)用自動(dòng)推理技術(shù)確保其云基礎(chǔ)設(shè)施和服務(wù)的正確性，同時(shí)增強(qiáng)其安全性和可靠性，并將設(shè)計(jì)缺陷最小化。開(kāi)發(fā)人員可以使用自動(dòng)推理為系統(tǒng)創(chuàng)建一個(gè)精確且可測(cè)試的模型，使用該模型快速驗(yàn)證更改是否安全，或者識(shí)別出安全隱患，以防止對(duì)生產(chǎn)環(huán)境造成不利影響。

借助自動(dòng)推理技術(shù)能夠發(fā)現(xiàn)并解決基礎(chǔ)設(shè)施的一些關(guān)鍵問(wèn)題，檢測(cè)可能導(dǎo)致數(shù)據(jù)泄露的錯(cuò)誤配置，阻止一些無(wú)法通過(guò)其它技術(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é)保證。

亞馬遜云科技在自動(dòng)推理領(lǐng)域擁有先進(jìn)的技術(shù)和經(jīng)驗(yàn)積累，并大量投資提升其可用性和可擴(kuò)展性。自動(dòng)推理工具的可用性能增強(qiáng)其功能和采用率，同時(shí)驗(yàn)證云基礎(chǔ)設(shè)施的正確性，并吸引重視安全的客戶。自動(dòng)推理不僅提高安全性，還能加速提供高性能代碼，幫助客戶節(jié)省成本。

經(jīng)過(guò)10多年的實(shí)踐，我們發(fā)現(xiàn)驗(yàn)證過(guò)的代碼性能更佳，因?yàn)轵?yàn)證過(guò)程中的bug修復(fù)提升了代碼的運(yùn)行性能。自動(dòng)推理強(qiáng)化開(kāi)發(fā)者信心，激勵(lì)他們探索更深層次的優(yōu)化，這不僅簡(jiǎn)化了代碼的維護(hù)和操作，還顯著提升了系統(tǒng)的整體性能。

如今大規(guī)模云架構(gòu)的核心屬性，如安全、合規(guī)、可用性、持久性和防護(hù)等，都能通過(guò)自動(dòng)化的方式得到驗(yàn)證。亞馬遜云科技的獨(dú)特之處在于，能從始至終運(yùn)用堅(jiān)實(shí)的數(shù)學(xué)推理，并持續(xù)不斷地分析構(gòu)建的每一個(gè)環(huán)節(jié)，預(yù)防從AI幻覺(jué)到虛擬機(jī)監(jiān)控程序、密碼學(xué)和分布式系統(tǒng)中可能出現(xiàn)的潛在問(wèn)題。