This paper focuses on assessing the end-to-end security properties of real-life SNARK (Succinct Non-Interactive Argument of Knowledge) implementations. It begins by establishing a system model and threat models, defining adversarial roles for systems that use SNARKs. The study analyzes 141 actual vulnerabilities in SNARK implementations, providing a detailed taxonomy to help developers and security researchers understand the security threats in systems employing SNARKs. The paper evaluates existing defense mechanisms and offers recommendations for enhancing the security of SNARK-based systems. Key findings include: - Developers struggle with correctly implementing arithmetic circuits, leading to common vulnerabilities such as input validation errors and over/underflows. - The unique programming model for SNARK circuits poses challenges, often resulting in under-constrained circuits. - Design and implementation errors in proof systems are critical but often overlooked. The paper contributes with: - A system and threat model for SNARKs. - A systematic study of known vulnerabilities in SNARK systems. - A taxonomy for classifying vulnerabilities in SNARKs. - An analysis of defense techniques and their gaps. The paper highlights that SNARKs are not just "math" but complex, compositional systems where cross-layer interactions can introduce vulnerabilities. It provides insights into the challenges and potential mitigations for improving the security of SNARK-based systems.This paper focuses on assessing the end-to-end security properties of real-life SNARK (Succinct Non-Interactive Argument of Knowledge) implementations. It begins by establishing a system model and threat models, defining adversarial roles for systems that use SNARKs. The study analyzes 141 actual vulnerabilities in SNARK implementations, providing a detailed taxonomy to help developers and security researchers understand the security threats in systems employing SNARKs. The paper evaluates existing defense mechanisms and offers recommendations for enhancing the security of SNARK-based systems. Key findings include: - Developers struggle with correctly implementing arithmetic circuits, leading to common vulnerabilities such as input validation errors and over/underflows. - The unique programming model for SNARK circuits poses challenges, often resulting in under-constrained circuits. - Design and implementation errors in proof systems are critical but often overlooked. The paper contributes with: - A system and threat model for SNARKs. - A systematic study of known vulnerabilities in SNARK systems. - A taxonomy for classifying vulnerabilities in SNARKs. - An analysis of defense techniques and their gaps. The paper highlights that SNARKs are not just "math" but complex, compositional systems where cross-layer interactions can introduce vulnerabilities. It provides insights into the challenges and potential mitigations for improving the security of SNARK-based systems.