Byron Cook，亞馬遜云科(ke)(ke)技(ji)自動(dong)推理副總裁及杰出科(ke)(ke)學家

北京2024年(nian)11月13日 /美通社/ -- 亞馬遜云科技是唯一一家如此大規模使用自動推理的云提供商。隨著越來越多的人使用自動推理工具，這讓我們在提升自動推理工具的可用性和可擴展性上更容易進行大量的投入。我們發現自動推理工具越易于使用，它們的功能就會變得越強大，同時自動推理工具的采用率也會變得越高。我們越能證明云基礎設施的正確性，對于那些看重安全的客戶而言我們的云就越有吸引力。正如本文所述，通過自動推理，我們不僅能夠提高安全性，還能更快地為客戶提供更高性能的代碼，并最終節省客戶的成本。

在亞馬遜云(yun)科技應用自動推理的10多年(nian)時(shi)間里(li)，我們(men)發現經(jing)過驗證(zheng)的代碼通(tong)常(chang)比它(ta)所替代的未經(jing)驗證(zheng)的代碼性能更好。

這(zhe)主要(yao)是因為在驗(yan)證過程中我們(men)所做的(de)bug修復通常會提升代(dai)碼(ma)的(de)運行(xing)性能。自動推理讓開發(fa)人(ren)員有信(xin)心去探索(suo)額外的(de)優化，進一步提升系(xi)統(tong)性能。我們(men)發(fa)現(xian)驗(yan)證的(de)代(dai)碼(ma)更(geng)容(rong)易更(geng)新、修改和操作，這(zhe)減少了半夜(ye)的(de)日志分析和調(diao)試(shi)環節。

自動推理的基本概念

在亞馬遜云(yun)科(ke)技，我們努力為(wei)客戶(hu)構建簡單、易(yi)用的(de)(de)(de)服務。但在這種簡單的(de)(de)(de)背(bei)后(hou)卻是(shi)(shi)龐大、復雜的(de)(de)(de)分(fen)布式系(xi)統，每秒處理(li)著(zhu)(zhu)數十億個請求。驗證這些復雜系(xi)統的(de)(de)(de)正(zheng)確(que)性是(shi)(shi)一(yi)個極(ji)大的(de)(de)(de)挑戰。我們的(de)(de)(de)服務隨著(zhu)(zhu)新功能(neng)的(de)(de)(de)增(zeng)加(jia)、組件的(de)(de)(de)重新設計、安(an)全的(de)(de)(de)增(zeng)強(qiang)和(he)性能(neng)的(de)(de)(de)優化，一(yi)直處于不斷變化和(he)發(fa)展的(de)(de)(de)狀態。很多變化本(ben)身就(jiu)是(shi)(shi)非常復雜的(de)(de)(de)，必須在不影響亞馬遜云(yun)科(ke)技本(ben)身或(huo)客戶(hu)的(de)(de)(de)安(an)全性和(he)韌性的(de)(de)(de)前提下進行。

設(she)計評審、代碼(ma)審計、壓力測試和(he)故障注入(ru)是我(wo)們經常以(yi)及未來都(dou)會一直使(shi)(shi)用的(de)(de)寶貴(gui)工具。然而，我(wo)們發現仍然需(xu)要(yao)使(shi)(shi)用額外的(de)(de)技(ji)術來確認許多情況下的(de)(de)正(zheng)確性。細微的(de)(de)bug仍可能逃(tao)過檢測，尤其是在大規模、容錯架構中(zhong)。有些問(wen)題甚至(zhi)可能源(yuan)于(yu)(yu)最初的(de)(de)系統(tong)設(she)計，而不是實施缺陷。隨著我(wo)們服務(wu)規模和(he)復雜(za)性的(de)(de)增長，我(wo)們不得(de)不使(shi)(shi)用基于(yu)(yu)數學和(he)邏輯的(de)(de)更(geng)強大技(ji)術作為(wei)對(dui)傳統(tong)測試方(fang)法的(de)(de)補充。這(zhe)就是人工智能(AI)的(de)(de)一個(ge)分支自動推理發揮作用的(de)(de)地方(fang)。

傳統(tong)(tong)(tong)測試側重(zhong)于在(zai)特定場(chang)景(jing)下(xia)驗證系(xi)統(tong)(tong)(tong)行為(wei)，而自(zi)動推理旨在(zai)使用邏輯(ji)來(lai)驗證系(xi)統(tong)(tong)(tong)在(zai)任何可能(neng)場(chang)景(jing)下(xia)的(de)(de)(de)(de)(de)行為(wei)。即使是(shi)(shi)一(yi)個中等(deng)復雜的(de)(de)(de)(de)(de)系(xi)統(tong)(tong)(tong)，要重(zhong)現可能(neng)發生的(de)(de)(de)(de)(de)每一(yi)種可能(neng)狀態和參數的(de)(de)(de)(de)(de)組合，所(suo)需的(de)(de)(de)(de)(de)時間也是(shi)(shi)難以想(xiang)象的(de)(de)(de)(de)(de)。自(zi)動推理可以通(tong)過計算(suan)系(xi)統(tong)(tong)(tong)正確(que)性(xing)的(de)(de)(de)(de)(de)邏輯(ji)證明(ming)來(lai)快速、高效地取得(de)相同的(de)(de)(de)(de)(de)效果(guo)。

使(shi)用(yong)自動推理需要我(wo)們的(de)開發者(zhe)具有(you)不同的(de)思維方式。我(wo)們不是試圖考慮所有(you)可能(neng)的(de)輸(shu)入場景及其可能(neng)出(chu)錯的(de)方式，而是定義系統應該如何工作，并識別出(chu)讓它正確(que)運(yun)行必須滿足的(de)條件(jian)。然后，我(wo)們可以使(shi)用(yong)數學證(zheng)明來驗證(zheng)這些條件(jian)是否為真。換句話說，我(wo)們可以驗證(zheng)系統是否正確(que)。

自動推(tui)理(li)將系(xi)統(tong)(tong)(tong)(tong)的規(gui)(gui)(gui)范和(he)實施以數(shu)學的形式進行(xing)審核，然后使(shi)用(yong)算法(fa)來驗證(zheng)系(xi)統(tong)(tong)(tong)(tong)的數(shu)學表示是(shi)否(fou)滿足規(gui)(gui)(gui)范。通過把我們的系(xi)統(tong)(tong)(tong)(tong)編(bian)碼為數(shu)學系(xi)統(tong)(tong)(tong)(tong)，并使(shi)用(yong)形式邏輯對其(qi)進行(xing)推(tui)理(li)，自動推(tui)理(li)使(shi)我們能(neng)夠有效和(he)權威地解答有關(guan)系(xi)統(tong)(tong)(tong)(tong)未來行(xing)為的關(guan)鍵問題。系(xi)統(tong)(tong)(tong)(tong)能(neng)做什(shen)么(me)？它將做什(shen)么(me)？它永遠不會(hui)做什(shen)么(me)？自動推(tui)理(li)可以幫助回答系(xi)統(tong)(tong)(tong)(tong)的這些問題，即便是(shi)最(zui)復雜的、大規(gui)(gui)(gui)模的和(he)潛(qian)在無限的系(xi)統(tong)(tong)(tong)(tong)——這些場景是(shi)單單通過傳統(tong)(tong)(tong)(tong)測試無法(fa)徹底(di)驗證(zheng)的。

自(zi)動(dong)推(tui)理能(neng)讓我們(men)達到(dao)完(wan)美的程度嗎？不能(neng)，因為它仍然依賴于(yu)對(dui)系統(tong)組件的正(zheng)確(que)行為以(yi)(yi)及系統(tong)與其環境模(mo)型(xing)之間關系的某些(xie)假(jia)設(she)。例如，系統(tong)模(mo)型(xing)可能(neng)錯(cuo)誤地假(jia)設(she)底(di)層(ceng)組件（如編譯器(qi)和處理器(qi)）沒有任(ren)何bug（盡管也可以(yi)(yi)對(dui)這(zhe)些(xie)組件進行驗證）。話雖如此，與使用(yong)傳統(tong)軟件開發(fa)和測(ce)試方法相比(bi)，自(zi)動(dong)推(tui)理讓我們(men)更有信(xin)心達到(dao)正(zheng)確(que)性。

更快的開發

自(zi)動(dong)推理(li)不僅(jin)僅(jin)是數學家和科學家的(de)工具。我(wo)們(men)的(de)  工程師每天都在(zai)使用(yong)自(zi)動(dong)推理(li)來防止bug。S3的(de)背后是世界(jie)上最大(da)、最復雜的(de)分(fen)布式系(xi)統(tong)之一，它存儲(chu)了400萬(wan)億個對象(xiang)、EB級別的(de)數據并通常需要每秒(miao)處理(li)1.5億個請求。S3由(you)許多(duo)子系(xi)統(tong)組(zu)成，這(zhe)些(xie)子系(xi)統(tong)本身就(jiu)是分(fen)布式系(xi)統(tong)，其中(zhong)許多(duo)由(you)數萬(wan)臺機器(qi)組(zu)成。S3一直不斷增加(jia)新的(de)功能，同時它也被我(wo)們(men)的(de)客(ke)戶大(da)量使用(yong)中(zhong)。

S3索(suo)引子(zi)系統(tong)是S3的(de)(de)一個關鍵組件，它是一個對(dui)象元數(shu)(shu)據存儲，來支持快速(su)的(de)(de)數(shu)(shu)據查找(zhao)。該組件包含一個非常大(da)的(de)(de)、復雜的(de)(de)數(shu)(shu)據結(jie)構和(he)精密的(de)(de)優化算(suan)法。以S3的(de)(de)這種大(da)規模，這些算(suan)法對(dui)于人類來說很難正確使(shi)用，同時(shi)我們也不能容許(xu)S3在查找(zhao)時(shi)發生任(ren)何錯誤，為此(ci)我們大(da)約每個季度都(dou)會進(jin)行新的(de)(de)改(gai)進(jin)，但任(ren)何更改(gai)都(dou)是在極其(qi)謹慎和(he)大(da)量(liang)測試的(de)(de)前提下進(jin)行的(de)(de)。

基于我們15年的(de)經(jing)驗(yan)，S3是一個(ge)構建良好(hao)以(yi)及經(jing)過充分測試(shi)的(de)系統(tong)(tong)。然而，我們曾一度無法確認S3索引子(zi)系統(tong)(tong)中一個(ge)bug的(de)根本原(yuan)因。該系統(tong)(tong)能夠從異常中自動(dong)恢(hui)復，因此該bug的(de)存在(zai)并沒有影響系統(tong)(tong)的(de)行為。但我們并不滿足于此。

為什么(me)這(zhe)個(ge)bug存在這(zhe)么(me)久？像(xiang)S3這(zhe)樣的(de)(de)(de)(de)分布(bu)式系(xi)統擁有大量組(zu)(zu)(zu)件，每個(ge)組(zu)(zu)(zu)件都(dou)有自(zi)己的(de)(de)(de)(de)異常(chang)(chang)情(qing)(qing)(qing)況(kuang)(kuang)（corner cases），而且有可(ke)(ke)能同時發生很多異常(chang)(chang)情(qing)(qing)(qing)況(kuang)(kuang)。就S3而言，它(ta)擁有超過300個(ge)微服務，這(zhe)些異常(chang)(chang)情(qing)(qing)(qing)況(kuang)(kuang)的(de)(de)(de)(de)潛在組(zu)(zu)(zu)合(he)的(de)(de)(de)(de)數(shu)量是巨大的(de)(de)(de)(de)。即使開(kai)發人(ren)員有證據證明bug存在，并可(ke)(ke)能知道引(yin)起bug的(de)(de)(de)(de)根(gen)本(ben)原(yuan)因，但(dan)對于開(kai)發人(ren)員來說，他(ta)們不(bu)可(ke)(ke)能考慮(lv)到所有異常(chang)(chang)情(qing)(qing)(qing)況(kuang)(kuang)，更(geng)不(bu)用說這(zhe)些異常(chang)(chang)情(qing)(qing)(qing)況(kuang)(kuang)的(de)(de)(de)(de)不(bu)同組(zu)(zu)(zu)合(he)了(le)。

這種復雜(za)性(xing)促(cu)使(shi)我(wo)們(men)(men)探索(suo)如何使(shi)用自動(dong)推理(li)來(lai)探索(suo)可能隱藏在(zai)這些狀態中的可能狀態和錯誤。通(tong)過構建系統(tong)的正式規范(fan)，我(wo)們(men)(men)能夠找到bug并證明未來(lai)不(bu)(bu)存(cun)在(zai)此類(lei)bug。使(shi)用自動(dong)推理(li)也讓我(wo)們(men)(men)有(you)信心每一(yi)兩個(ge)月發(fa)布(bu)一(yi)次更新(xin)和改(gai)進，而(er)不(bu)(bu)是一(yi)年只發(fa)布(bu)三或四次。

更快的代碼

服務(wu)的(de)(de)正(zheng)確(que)(que)性是確(que)(que)保我們客(ke)戶(hu)工作(zuo)負載(zai)安(an)全(quan)(quan)的(de)(de)基(ji)礎。每(mei)個發送到亞(ya)馬遜(xun)(xun)云科(ke)技(ji)的(de)(de)請求即每(mei)個API 調用都由(you)IAM授權(quan)引(yin)擎處理，這(zhe)會涉及到數百(bai)萬客(ke)戶(hu)、數千種(zhong)(zhong)資源(yuan)類型和(he)數百(bai)種(zhong)(zhong)亞(ya)馬遜(xun)(xun)云科(ke)技(ji)的(de)(de)服務(wu)。這(zhe)種(zhong)(zhong)請求每(mei)秒就(jiu)超過12億次(ci)。這(zhe)是亞(ya)馬遜(xun)(xun)云科(ke)技(ji)中(zhong)對安(an)全(quan)(quan)要求最高(gao)以(yi)及需要高(gao)度擴展的(de)(de)軟件(jian)之(zhi)一(yi)。

在(zai)亞(ya)馬遜云科技，任何改變在(zai)進(jin)入到生(sheng)產環(huan)境之(zhi)前(qian)，我們(men)需要有(you)極高的信心確保(bao)系統(tong)保(bao)持安(an)全(quan)和正確。使用(yong)自動推(tui)理(li)，我們(men)可以證(zheng)(zheng)明(ming)我們(men)的系統(tong)在(zai)幾乎所有(you)情(qing)況下遵(zun)守特定的安(an)全(quan)屬性(xing)。我們(men)稱之(zhi)為可證(zheng)(zheng)明(ming)的安(an)全(quan)性(xing)。自動推(tui)理(li)不僅使我們(men)能(neng)(neng)夠(gou)為客戶提供可證(zheng)(zheng)明(ming)的安(an)全(quan)保(bao)證(zheng)(zheng)，還讓我們(men)能(neng)(neng)夠(gou)大規模交付(fu)功能(neng)(neng)、安(an)全(quan)性(xing)和優化。

與(yu)S3一樣，IAM在(zai)過(guo)去超過(guo)15年時(shi)(shi)間里，已經(jing)成為(wei)(wei)一個(ge)(ge)(ge)經(jing)過(guo)時(shi)(shi)間考驗的(de)、值得信賴的(de)系(xi)統。但我們想進一步提高標準。我們構建了(le)一個(ge)(ge)(ge)正式規范來(lai)捕(bu)獲現有IAM授(shou)權引擎(qing)的(de)行為(wei)(wei)，將其策略評估原則(ze)編(bian)碼為(wei)(wei)可證(zheng)明的(de)定理(li)，并使(shi)(shi)用(yong)自動推理(li)構建了(le)一個(ge)(ge)(ge)新(xin)的(de)、更高效的(de)實施(shi)。今年早些時(shi)(shi)候，我們部署(shu)了(le)新(xin)的(de)經(jing)過(guo)證(zheng)明正確(que)的(de)授(shou)權引擎(qing)——沒人注意(yi)到。自動推理(li)使(shi)(shi)我們能夠(gou)無縫(feng)地用(yong)經(jing)證(zheng)明正確(que)的(de)替(ti)換(huan)物代替(ti)授(shou)權引擎(qing)，一個(ge)(ge)(ge)最關鍵的(de)亞馬遜云科(ke)技(ji)基礎(chu)設施(shi)之一。

有了(le)規范和(he)證(zheng)明(ming)，我(wo)(wo)們可以很(hen)有信(xin)心的(de)(de)安全、積極地優化代碼。在IAM的(de)(de)大規模下，每一微(wei)秒(miao)的(de)(de)性(xing)能改(gai)進都意味著更(geng)(geng)好的(de)(de)客(ke)戶體驗和(he)我(wo)(wo)們自身更(geng)(geng)好的(de)(de)成(cheng)本優化。我(wo)(wo)們優化了(le)字符串匹配(pei)、刪(shan)除了(le)不必要的(de)(de)內存分(fen)配(pei)和(he)冗余計算、加強了(le)安全性(xing)并提高(gao)了(le)可擴(kuo)展性(xing)。每次更(geng)(geng)新后，我(wo)(wo)們都會再次運行(xing)證(zheng)明(ming)，來確認(ren)系統仍在正確運行(xing)。

現在(zai)，優化后(hou)的IAM授權引擎相(xiang)比之前快了(le)50%。如果不使用自動推理，我(wo)們根本不可能這么(me)有信心地(di)進行如此重要的優化。

更快的代碼部署

大多(duo)數(shu)(shu)(shu)(shu)在線安(an)全(quan)交易都受(shou)到加(jia)密(mi)保護。例如，RSA加(jia)密(mi)算法(fa)通過生成兩個(ge)(ge)(ge)密(mi)鑰來保護數(shu)(shu)(shu)(shu)據(ju)(ju)(ju)：一(yi)(yi)(yi)個(ge)(ge)(ge)用(yong)于加(jia)密(mi)數(shu)(shu)(shu)(shu)據(ju)(ju)(ju)，另一(yi)(yi)(yi)個(ge)(ge)(ge)用(yong)于解密(mi)數(shu)(shu)(shu)(shu)據(ju)(ju)(ju)。這(zhe)些密(mi)鑰實現了安(an)全(quan)的(de)(de)數(shu)(shu)(shu)(shu)據(ju)(ju)(ju)傳輸以及安(an)全(quan)的(de)(de)數(shu)(shu)(shu)(shu)字簽名。在加(jia)密(mi)這(zhe)種場(chang)景下(xia)，正確(que)性(xing)和性(xing)能(neng)至(zhi)關重要——加(jia)密(mi)算法(fa)中(zhong)的(de)(de)一(yi)(yi)(yi)個(ge)(ge)(ge)bug可(ke)能(neng)是(shi)災難(nan)性(xing)的(de)(de)。

隨著亞馬遜云科技客(ke)戶(hu)將(jiang)工(gong)作負載遷(qian)移到Amazon Graviton上(shang)，針對ARM指(zhi)令集的(de)密(mi)(mi)碼優(you)化(hua)的(de)好處也得(de)到凸顯。但是(shi)，通過加(jia)密(mi)(mi)優(you)化(hua)獲得(de)更好的(de)性(xing)能(neng)(neng)是(shi)很(hen)復(fu)雜的(de)，這使(shi)得(de)驗證修改(gai)后的(de)加(jia)密(mi)(mi)算(suan)法(fa)是(shi)否正常運行(xing)變(bian)得(de)困難。在我們(men)開始使(shi)用自動(dong)推理之前(qian)，對密(mi)(mi)碼學庫(ku)進行(xing)優(you)化(hua)通常需要數月的(de)審查，才能(neng)(neng)獲得(de)足夠(gou)的(de)信心(xin)將(jiang)其(qi)投入(ru)生產環(huan)境。

自動(dong)推理(li)的(de)力量就(jiu)在于此：正式驗證使(shi)RSA更快，部(bu)署(shu)也更快。當我(wo)們將自動(dong)推理(li)應用(yong)于橢圓曲線密(mi)碼學(xue)時，我(wo)們也看到(dao)了類似(si)的(de)提升。

形成一個良性循環

我們在(zai)過去十多年間，在(zai)亞馬(ma)遜云科技(ji)的(de)內部越來越多的(de)應用(yong)(yong)自動推理技(ji)術來證明我們的(de)云基礎設(she)施和(he)服務的(de)正確(que)性(xing)。我們經常使(shi)用(yong)(yong)這些方法不僅用(yong)(yong)于驗證正確(que)性(xing)，而且還用(yong)(yong)于增(zeng)強安(an)全性(xing)和(he)可靠性(xing)，以及最小化設(she)計缺陷。可以使(shi)用(yong)(yong)自動推理為一個系統創(chuang)建一個精確(que)且可測(ce)試的(de)模型，使(shi)用(yong)(yong)該模型快(kuai)速驗證更(geng)改是否安(an)全，或者發現它們是不安(an)全的(de)來避免對生(sheng)產(chan)環(huan)節產(chan)生(sheng)有(you)害影響。

我(wo)(wo)們(men)(men)可以(yi)回答關于我(wo)(wo)們(men)(men)基礎(chu)設施的(de)一些關鍵(jian)問題，來檢測可能導(dao)致(zhi)數據泄露的(de)錯誤(wu)配置(zhi)。我(wo)(wo)們(men)(men)可以(yi)阻(zu)止(zhi)一些我(wo)(wo)們(men)(men)無法通過其他技術發現的(de)微妙(miao)但(dan)嚴重的(de)錯誤(wu)進入生產環境。有了模(mo)型檢查，我(wo)(wo)們(men)(men)獲得了顯著的(de)性能優化(hua)，這是我(wo)(wo)們(men)(men)以(yi)往不敢嘗試的(de)。自(zi)動推(tui)理為關鍵(jian)系統(tong)按預(yu)期運行提(ti)供了嚴格的(de)數學(xue)保證。

亞馬遜云科技(ji)是唯一一家如此(ci)大(da)規模使用(yong)(yong)自(zi)動(dong)推(tui)理的(de)(de)(de)云提(ti)供商。隨著(zhu)越(yue)(yue)來越(yue)(yue)多的(de)(de)(de)人(ren)使用(yong)(yong)自(zi)動(dong)推(tui)理工具(ju)，這讓我(wo)(wo)(wo)們(men)在提(ti)升自(zi)動(dong)推(tui)理工具(ju)的(de)(de)(de)可(ke)用(yong)(yong)性(xing)和可(ke)擴展性(xing)上更容(rong)易進行(xing)大(da)量的(de)(de)(de)投(tou)入(ru)。我(wo)(wo)(wo)們(men)發現自(zi)動(dong)推(tui)理工具(ju)越(yue)(yue)易于使用(yong)(yong)，它們(men)的(de)(de)(de)功能(neng)就(jiu)會變(bian)得越(yue)(yue)強大(da)，同時自(zi)動(dong)推(tui)理工具(ju)的(de)(de)(de)采(cai)用(yong)(yong)率也會變(bian)得越(yue)(yue)高。我(wo)(wo)(wo)們(men)越(yue)(yue)能(neng)證(zheng)明云基(ji)礎設施的(de)(de)(de)正確性(xing)，對于那(nei)些看重安(an)全的(de)(de)(de)客戶(hu)而言我(wo)(wo)(wo)們(men)的(de)(de)(de)云就(jiu)越(yue)(yue)有吸引(yin)力。正如前文所述，我(wo)(wo)(wo)們(men)不僅(jin)能(neng)夠提(ti)高安(an)全性(xing)，還(huan)能(neng)更快地為客戶(hu)提(ti)供更高性(xing)能(neng)的(de)(de)(de)代碼，并最(zui)終節約客戶(hu)的(de)(de)(de)成本。

我們正處于一個新時(shi)代的(de)開端，在這個時(shi)代大規(gui)模(mo)云架構(gou)的(de)關鍵屬性，諸如安(an)全、合規(gui)性、可(ke)用性、持久性和防(fang)(fang)護等都可(ke)以實(shi)現自動證明。亞馬遜與眾不同之處就在于，我們從(cong)基礎就用可(ke)靠的(de)數學推理并持續分析我們所構(gou)建的(de)一切(qie)，防(fang)(fang)止從(cong)AI幻(huan)覺(jue)到分析虛擬機(ji)監控程序(xu)、密(mi)碼學和分布(bu)式(shi)系統(tong)等潛在問題的(de)發生。