academia

2024

1. 

   Assessing RISC Zero Using ZKit: An Extensible Testing and Benchmarking Suite for ZKP Frameworks

   Roman Bögli

   Jan 2024

   Abs Bib HTML PDF

   This thesis summarizes the most important properties of ZKPs and highlights the key differences between two famous implementation families, namely SNARK and STARK systems. Also, we provide a summary of promising software libraries or frameworks that help to create and verify ZKPs. Next, we analyze risc0 in detail using the above-addressed use case of an IP, i.e., proving a the inclusion of leaf in a Merkle tree data structure. Therefore, we propose the concept of ZKit, an extensible toolkit for testing and benchmarking various ZKP frameworks. Besides a Command Line Interface (CLI) to execute parameterized benchmarks or generate Merkle tree test data, it also contains functionality to define and exchange IPs in a unified way. Furthermore, ZKit exemplifies how ZKP circuits written in Rust can be ported to the Go ecosystem through a wrapper library. This portability facilitates the integration of ZKPs in existing Go projects such as for example the Fabric Token-SDK (FTS). Last but not least, we share our risc0 benchmark results on IPs in two different settings. In the first setting, we measured the performance and allocated resources to create one proof for a single IP. In the second setting, we aggregate or batch multiple IPs in a single proof. We compare and interpret the results of these two settings at the end and state our recommendations that we drew from it.

   @mastersthesis{bogli2024AssessingRISCZero,
     type = {Master {Thesis}},
     title = {Assessing {{RISC Zero}} Using {{ZKit}}: {{An Extensible Testing}} and {{Benchmarking Suite}} for {{ZKP Frameworks}}},
     author = {Bögli, Roman},
     editora = {El Khiyaoui, Kaoutar and De Caro, Angelo and Caracas, Alexandru},
     editoratype = {collaborator},
     date = {2024-01-23},
     month = jan,
     year = {2024},
     language = {English},
     school = {Eastern Switzerland University of Applied Science},
     url = {https://eprints.ost.ch/id/eprint/1158/},
   }

2. 

   A Systematic Literature Review on a Decade of Industrial TLA+ Practice

   Roman Bögli, Leandro Lerena, Christos Tsigkanos, and Timo Kehrer

   In Integrated Formal Methods, Nov 2024

   Abs DOI Bib Slides

   TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in practice remains scarce. Industry reports suggest that software engineers could benefit from insights, innovations, and solutions to the practical challenges of TLA+. This paper explores this development by conducting a systematic literature review of TLA+’s industrial usage over the past decade. We analyze the trend in industrial application, characterize its use, examine whether its promised benefits resonate with practitioners, and identify challenges that may hinder further adoption.

   @inproceedings{10.1007/978-3-031-76554-4_2,
     author = {B{\"o}gli, Roman and Lerena, Leandro and Tsigkanos, Christos and Kehrer, Timo},
     editor = {Kosmatov, Nikolai and Kov{\'a}cs, Laura},
     title = {A Systematic Literature Review on a Decade of Industrial TLA+ Practice},
     booktitle = {Integrated Formal Methods},
     month = nov,
     year = {2024},
     date = {2024-11-13},
     publisher = {Springer Nature Switzerland},
     address = {Cham},
     pages = {24--34},
     isbn = {978-3-031-76554-4},
     doi = {10.1007/978-3-031-76554-4_2},
   }

2023

1. 

   A Security Focused Outline on Bitcoin Wallets

   Roman Bögli

   Mar 2023

   Abs Bib HTML PDF

   The famous electronic peer-to-peer cash system called Bitcoin is an open-source protocol allowing individuals to store and transact units of the same named currency. Private and public key cryptography plays a central role in this value transfer system, which implies the importance of professionally managing the information about such keys. This work elaborates on the essential prerequisites to understand this relatively new technology that combines elements from the fields of computer science, cryptography, mathematics, and game theory. In doing so, crucial general and Bitcoin-specific terms are defined and contextually explained. The central part of this work addresses the outline of different Bitcoin interaction means, commonly known as wallets. The structure of the presented wallet types orients itself alongside a potential user’s experience. Besides defining explanations and examples of use cases, this work outlines advantages and disadvantages concerning security and privacy. The start concerns two wallets that target beginners in the field of Bitcoin. The concept of online accounts is elaborated and attention is drawn to the inherent need to trust when using them. Also, the relatively primitive type of paper wallets is surveyed. For a more intermediate interaction with this peer-to-peer cash system, the concept of software wallets, in general, is explained and examples are provided. The bridge from single-address paper wallets will be drawn to the more sophisticated multi-address wallets enabled through rooted key derivation techniques. Designated computer devices that solely serve the purpose of managing keying material, known as hardware wallets, represent another intermediate wallet type discussed in this work. Last, advanced topics are discussed that further leverage the security and privacy of someone’s interaction with Bitcoin. One concerns the setup of a self-managed Bitcoin full node. This undertaking not only harmonies with the concept of verification over trust but also allows for the complete exclusion of any third party between wallet communication. Equally advanced is the concept of multi-signature wallets, which is discussed at the end of this work.

   @misc{bogli2023SecurityFocusedOutline,
     title = {A {Security} {Focused} {Outline} on {Bitcoin} {Wallets}},
     language = {en},
     publisher = {Eastern Switzerland University of Applied Science},
     author = {Bögli, Roman},
     collaborator = {Weiler, Nathalie},
     date = {2023-03-07},
     month = mar,
     year = {2023},
     url = {https://eprints.ost.ch/id/eprint/1103/},
   }

2. 

   Zero-Knowledge Inclusion Proofs

   Roman Bögli

   Aug 2023

   Abs Bib HTML PDF

   This work discusses a solution for implementing a zero-knowledge inclusion proof using existing software components, referred to as automation frameworks. In the beginning, the use case that necessitates such proofs is stated together with establishing the contextual backdrop. This includes elaborating essential prerequisites such as cryptographic hash functions, commitment schemes, and Merkle trees. Furthermore, it presents an overview of zero-knowledge proof systems, detailing their core characteristics, analogies, and real-world applications. The discussion delves into the two prominent implementation families, namely zkSNARK and zkSTARK, emphasizing their distinguishing features. To ensure resistance against potential threats originating from quantum computers, the proposed approach centers on utilizing non-interactively employed zkSTARK proofs enabled through the Fiat-Shamir transformation. Finally, this work formally states the objective of the zero-knowledge inclusion proof for the specific use case and proposes an algorithmic specification. A curated selection of promising automation frameworks with the potential to facilitate the objective’s implementation is presented, with in-depth scrutiny applied to two specific frameworks: RISC Zero and the Winterfell. The work concludes by discussing initial experiences with these frameworks and outlining future endeavors to chart the path towards implementing a minimal viable product.

   @misc{bogli2023ZeroKnowledgeInclusionProofs,
     title = {Zero-{Knowledge} {Inclusion} {Proofs}},
     language = {EN},
     publisher = {Eastern Switzerland University of Applied Science},
     author = {Bögli, Roman},
     collaborator = {El Khiyaoui, Kaoutar and De Caro, Angelo and Purandare, Mitra},
     date = {2023-08-21},
     month = aug,
     year = {2023},
     url = {https://eprints.ost.ch/id/eprint/1121/},
   }

2020

1. 

   Time Series Clustering with Water Temperature Data

   Roman Bögli

   Aug 2020

   Abs Bib HTML PDF

   This thesis studies three different approaches to cluster long-term water temperature data using the unsupervised pattern recognition method called hierarchical clustering. The cluster qualities are assessed using internal cluster validity indexes and forecast deviation analysis.

   @thesis{bogli2020TimeSeriesClustering,
     type = {Bachelor {Thesis}},
     title = {Time {Series} {Clustering} with {Water} {Temperature} {Data}},
     language = {English},
     school = {University of Applied Sciences and Arts Northwestern Switzerland (FHNW)},
     author = {Bögli, Roman},
     collaborator = {Bigler, Vidushi C.},
     date = {2020-08-07},
     month = aug,
     year = {2020},
     url = {https://studierendenprojekte.wirtschaft.fhnw.ch/view/61},
   }

2019

1. 

   Statistical vs. Structural Pattern Recognition - A Survey

   Roman Bögli

   Dec 2019

   Abs Bib PDF

   This paper surveys the different approaches in pattern recognition (PR). After the fundamental idea of PR is stated, a taxonomy landscape is presented which divides into three families, namely statistical, structural, and hybrids. The first represents a well-researched topic in PR which engendered popular and efficient supervised and unsupervised pattern discovery algorithms. The second family addresses techniques to find patterns in structurally represented data using graphs that allow capturing the information of relationships among objects. Thirdly, the hybridization of the prior two families will be discussed. This includes the elaboration of transformation methods that allow to embed a graph into a vector space using graph kernels or graph embedding.

   @misc{bogli2019StatisticalVsStructural,
     type = {Literature {Review}},
     title = {Statistical vs. {Structural} {Pattern} {Recognition} - {A} {Survey}},
     language = {English},
     publisher = {University of Applied Science and Arts Northwestern Switzerland (FHNW)},
     author = {Bögli, Roman},
     date = {2019-12-24},
     month = dec,
     year = {2019},
   }