來自奧地利維也納科技大學的研究團隊，打造了一個用於分析瀏覽器安全的安全框架：WebSpec。團隊利用WebSpec找出多個影響網頁瀏覽器的邏輯缺陷，更發現一種利用cookie的新型態攻擊，以及網頁內容安全政策（Content Security Policy，CSP）的內部矛盾。
邏輯缺陷意指網頁平臺程式規格與網頁瀏覽器實際套用的程式規格不一致。雖然邏輯缺陷不一定等於安全弱點，但仍很有可能成為安全弱點。
維也納科大開發WebSpec的目標，是用自動化、可驗證的檢查規則取代手動審查，進而加強網頁安全。在團隊發表的學術論文〈WebSpec：邁向瀏覽器安全機制的機器檢查分析〉（WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms）中，他們解釋，隨著網頁平臺新增越來越多元件，瀏覽器也變得益發複雜。
新開發的網頁平臺元件必須經過規格測試，確認能否與既有API及不同瀏覽器互通運作。過去，這些測試都是由技術專家手動執行。團隊指出，人工測試容易忽略程式邏輯的缺陷，進而導致重大安全弱點。
WebSpec使用Coq定理證明程式工具，以標準規格檢查瀏覽器與程式規格定義的行為。團隊也設定10個「網頁平臺在更新及平臺元件交互作用時，皆應獨立不變動的性質」，又稱為不變值（invariant），以檢查網頁程式規格與瀏覽器之間不一致之處。
根據團隊研究，WebSpec不只能執行更詳盡的自動化檢查，還發現了針對使用_Host-前綴cookie的新型攻擊，以及內容安全政策中繼承規則與HTML標準規劃變動的不一致。
有了WebSpec這個正規化瀏覽器行為檢測的工具，過去因瀏覽器程式碼不斷擴充而疲於維護的技術人員，或將得以卸下部分重擔。
相關連結：
Thomas Claburn (2022). WebSpec, a formal framework for browser security analysis, reveals new cookie attack. The Register.
檢自：
https://www.theregister.com/2022/01/08/webspec_browser_security/ (Jan. 17 , 2022)
