Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) serves as a powerful technique for proving the correctness of computations and has attracted significant interest from researchers. Numerous concrete schemes and implementations have been proposed in academia and industry. Unfortunately, the inherent complexity of zk-SNARK has created gaps between researchers, developers and users, as they focus differently on this technique. For example, researchers are dedicated to constructing new efficient proving systems with stronger security and new properties. At the same time, developers and users care more about the implementation's toolchains, usability and compatibility. This gap has hindered the development of zk-SNARK field. In this work, we provide a comprehensive study of zk-SNARK, from theory to practice, pinpointing gaps and limitations. We first present a master recipe that unifies the main steps in converting a program into a zk-SNARK. We then classify existing zk-SNARKs according to their key techniques. Our classification addresses the main difference in practically valuable properties between existing zk-SNARK schemes. We survey over 40 zk-SNARKs since 2013 and provide a reference table listing their categories and properties. Following the steps in master recipe, we then survey 11 general-purpose popular used libraries. We elaborate on these libraries' usability, compatibility, efficiency and limitations. Since installing and executing these zk-SNARK systems is challenging, we also provide a completely virtual environment in which to run the compiler for each of them. We identify that the proving system is the primary focus in cryptography academia. In contrast, the constraint system presents a bottleneck in industry. To bridge this gap, we offer recommendations and advocate for the open-source community to enhance documentation, standardization and compatibility.

Signature schemes are a fundamental component of cybersecurity infrastructure. While they are designed to be mathematically secure against cryptographic attacks, they are vulnerable to Rowhammer fault-injection attacks. Since all existing attacks are ad-hoc in that they target individual parameters of specific signature schemes, it remains unclear about the impact of Rowhammer on signature schemes as a whole. In this paper, we present Achilles, a formal framework that aids in leaking secrets in various real-world signature schemes via Rowhammer. Particularly, Achilles can be used to find potentially more vulnerable parameters in schemes that have been studied before and also new schemes that are potentially vulnerable. Achilles mainly describes a formal procedure where Rowhammer faults are induced to key parameters of a generalized signature scheme, called G-sign, and a post-Rowhammer analysis is then performed for secret recovery on it. To illustrate the viability of Achilles, we have evaluated six signature schemes (with five CVEs assigned to track their respective Rowhammer vulnerability), covering traditional and post-quantum signatures with different mathematical problems. Based on the analysis with Achilles, all six schemes are proved to be vulnerable, and two new vulnerable parameters are identified for EdDSA. Further, we demonstrate a successful Rowhammer attack against each of these schemes, using recent cryptographic libraries including wolfssl, relic, and liboqs.