協(xié)議設計時產(chǎn)生的缺陷:嘗試寫一正式驗證PDF解析器時的發(fā)現(xiàn)

引用：

Bogk A, Sch?pl M. The Pitfalls of Protocol Design: Attempting to Write a Formally Verified PDF Parser[C]//Security and Privacy Workshops (SPW), 2014 IEEE. IEEE, 2014: 198-203.

研究內(nèi)容：

使用支持依賴類型的函數(shù)式編程語言實現(xiàn)正式驗證的PDF解析器

背景：

Coq是一個證明輔助工具,通過使用Coq提取代碼來編寫軟件是完全可行的;在信息安全技術(shù)的語言理論方向可以和依賴類型編程語言結(jié)合起來進行正式驗證

方法：

在起初的嘗試中發(fā)現(xiàn)Coq在驗證時不支持無限遞歸,接下來通過使用依賴類型定義parser，成功使得在解析過程中可以通過逐步消耗tokens實現(xiàn)遞歸
要使用上述的組合庫解析器實現(xiàn)一個PDF文檔解析器，在解析的PDF文檔部分結(jié)構(gòu)的時候非常容易實現(xiàn)，但是在解析完整的文檔時就會遇到遞歸調(diào)用問題，如對象的自調(diào)用和雙對象相互調(diào)用、增量交叉引用表的相互引用，而這可以使用此方法解決無限循環(huán)的問題

創(chuàng)新點：

使用Coq即函數(shù)式編程語言來解決PDF解析中存在的問題