請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8253
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 鄭振牟(Chen-Mou Cheng) | |
dc.contributor.author | Ruey-Lin Hsu | en |
dc.contributor.author | 許瑞麟 | zh_TW |
dc.date.accessioned | 2021-05-20T00:50:48Z | - |
dc.date.available | 2020-09-02 | |
dc.date.available | 2021-05-20T00:50:48Z | - |
dc.date.copyright | 2020-09-02 | |
dc.date.issued | 2020 | |
dc.date.submitted | 2020-08-12 | |
dc.identifier.citation | [1] D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, and N. Swamy. Recalling a witness: Foundations and applications of monotonic state. Proc. ACM Program. Lang., 2(POPL), Dec. 2017. [2] E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. Snarks for c: Verifying program executions succinctly and in zero knowledge. In R. Canetti and J. A. Garay, editors, Advances in Cryptology – CRYPTO 2013, pages 90–108, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [3] E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza. Succinct non-interactive zero knowledge for a von neumann architecture. In Proceedings of the 23rd USENIX Conference on Security Symposium, SEC’14, page 781 – 796, USA, 2014. USENIX Association. [4] E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23:552–593, 9 2013. [5] J. Cockx, D. Devriese, and F. Piessens. Pattern matching without K. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP ’14, pages 257–268, New York, NY, USA, 2014. Association for Computing Machinery. [6] P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000. [7] C. Fournet, C. Keller, and V. Laporte. A certified compiler for verifiable computing. In 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pages 268–280, June 2016. [8] R. Gennaro, C. Gentry, B. Parno, and M. Raykova. Quadratic span programs and succinct nizks without pcps. In T. Johansson and P. Q. Nguyen, editors, Advances in Cryptology – EUROCRYPT 2013, pages 626–645, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [9] H. Goguen, C. McBride, and J. McKinna. Eliminating Dependent Pattern Matching, pages 521–540. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. [10] R. J. M. Hughes. A novel representation of lists and its application to the function “reverse”. Inf. Process. Lett., 22(3):141 – 144, Mar. 1986. [11] P. Martin-Löf. An intuitionistic theory of types. Technical report, University of Stockholm, 1972. [12] C. McBride. Elimination with a motive. In P. Callaghan, Z. Luo, J. McKinna, R. Pollack, and R. Pollack, editors, Types for Proofs and Programs, pages 197–216, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. [13] U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007. [14] G. Stewart, S. Merten, and L. Leland. Snårkl: Somewhat practical, pretty much declarative verifiable computing in haskell. In F. Calimeri, K. Hamlen, and N. Leone, editors, Practical Aspects of Declarative Languages, pages 36–52, Cham, 2018. Springer International Publishing. [15] The Coq Development Team. The Coq proof assistant, Jan. 2020. [16] Zokrates Development Team. Zokrates. https://github.com/Zokrates/ ZoKrates. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/8253 | - |
dc.description.abstract | 本論文提出一個依值型別的可驗證計算編譯器,並證明其可靠性。此編譯器將一個淺層嵌入於 Agda 當中,具有依值型別的領域特定語言轉換成一階限制條件。可靠性是轉換正確性的一個部份,表示如果產生出來的限制條件是可被滿足的,那產生出來的限制條件會是正確的。藉由利用柯里-霍華德對應,我們在互動式定理證明器 Agda 當中建構此編譯器的形式規格以及證明其可靠性。 | zh_TW |
dc.description.abstract | In this thesis, we will construct and prove the soundness of a dependently typed verifiable computation compiler. The compiler described in this thesis compiles a user program written in a dependently typed shallowly embedded domain specific language in Agda into a set of rank 1 constraints. Soundness is a part of translational correctness that says that if the generated constraints are satisfiable, then the generated constraints are correct. By utilizing the Curry-Howard correspondence, the compiler is formally specified and proved in the interactive theorem prover Agda. | en |
dc.description.provenance | Made available in DSpace on 2021-05-20T00:50:48Z (GMT). No. of bitstreams: 1 U0001-1108202022141900.pdf: 679722 bytes, checksum: 895e903f12be4f371b94d5154a11310a (MD5) Previous issue date: 2020 | en |
dc.description.tableofcontents | 誌謝 iii Acknowledgements v 摘要 vii Abstract ix 1 Introduction 1 2 Background 5 2.1 Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Verifiable Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Constructing an Embedded Type Universe 13 3.1 Type Code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2 List Membership . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.3 Counting Number of Occurrences . . . . . . . . . . . . . . . . . . . . . 16 3.4 Finite Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.5 Field . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.6 List Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.6.1 Properties of List Monad . . . . . . . . . . . . . . . . . . . . . . 19 3.7 Enumerating Elements of Embedded Types . . . . . . . . . . . . . . . . 22 3.7.1 Enumerating Elements of Embedded Pi Types . . . . . . . . . . . 22 3.7.2 Defining Enumeration of Elements of Embedded Types . . . . . 30 3.7.3 Uniqueness of Elements in enum . . . . . . . . . . . . . . . . . . 31 3.8 Size of Type Codes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4 Source EDSL 37 4.1 Source . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.2 RWS Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.3 S-Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3.1 S-Monad Utilities . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.3.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 5 Compiling Programs From Source to R1CS 53 5.1 RWSInvMonad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.2 SI-Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 5.3 Basic Utilities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 5.4 Basic Logic Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 5.5 Auxiliary Compilation Functions . . . . . . . . . . . . . . . . . . . . . . 63 5.6 Main Compilation Functions . . . . . . . . . . . . . . . . . . . . . . . . 65 5.6.1 Generating Type Constraints . . . . . . . . . . . . . . . . . . . . 67 5.7 Compiling Source to R1CS . . . . . . . . . . . . . . . . . . . . . . . . . 69 6 Formal Verification of the Compiler 73 6.1 Solution of R1CS Constraints . . . . . . . . . . . . . . . . . . . . . . . . 76 6.2 Literal Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 6.3 Semantics Function for Source . . . . . . . . . . . . . . . . . . . . . . . 80 6.4 Compilation Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 7 Conclusion 89 A Full Definition of enum 91 B Additional Formal Verification Lemmas and Definitions 95 Bibliography 127 | |
dc.language.iso | en | |
dc.title | 形式化驗證零知識證明系統編譯器 | zh_TW |
dc.title | From a Dependently Typed Language to ZK-SNARKs Circuits: A Formally Verified Compiler | en |
dc.type | Thesis | |
dc.date.schoolyear | 108-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 楊柏因(Bo-Yin Yang),穆信成(Shin-Cheng Mu),柯向上(Hsiang-Shang Ko) | |
dc.subject.keyword | 依值型別程式設計,互動式定理證明器,可驗證計算,形式化驗證,Agda, | zh_TW |
dc.subject.keyword | dependently typed programming,interactive theorem prover,verifiable computation,formal verification,Agda, | en |
dc.relation.page | 128 | |
dc.identifier.doi | 10.6342/NTU202003013 | |
dc.rights.note | 同意授權(全球公開) | |
dc.date.accepted | 2020-08-12 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
U0001-1108202022141900.pdf | 663.79 kB | Adobe PDF | 檢視/開啟 |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。