Zero-Knowledge Location Privacy via Accurate Floating-Point SNARKs

Zero-Knowledge Location Privacy via Accurate Floating-Point SNARKs

Speakers: Jens Ernstberger, Chengru Zhang, Luca Ciprian, Philipp Jovanovic, Sebastian Steinhorst

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=XXSB_WSTuss

Overview

In an era where location-based services (LBS) are deeply integrated into daily life, the pervasive collection and processing of geospatial data raise significant privacy concerns. From mapping applications and cellular networks to transportation platforms like Uber, individuals' precise location information is constantly gathered, often without adequate protection, leading to inadvertent or intentional leaks of sensitive data. This talk, presented by Chengru Zhang and co-authored with Jens Ernstberger, Luca Ciprian, Philipp Jovanovic, and Sebastian Steinhorst, addresses this critical privacy challenge by proposing a novel solution: zero-knowledge location privacy via accurate floating-point SNARKs.

The core innovation lies in a two-pronged approach: first, obfuscating exact user coordinates into an approximate region, and second, proving the legitimacy of this obfuscation using zero-knowledge proofs (ZKPs), specifically SNARKs (Succinct Non-interactive ARguments of Knowledge). The work introduces a new gadget for performing accurate floating-point arithmetic within SNARK circuits, which is crucial for handling the complex calculations inherent in geospatial indexing systems like Uber's H3 framework. This advancement ensures both the utility of approximate location data and the rigorous privacy guarantees of ZKPs, setting a new standard for location privacy in digital services.

Background

▶ Watch: Zero-knowledge location privacy: problem and solution (0:00)

The proliferation of gadgets equipped with location sensors – mobile phones, tracking devices, and IoT devices – has led to the accumulation of vast datasets of location information. While these datasets are invaluable for developing and refining services across various sectors, the privacy implications are profound. Historical incidents have repeatedly demonstrated the vulnerability of precise location data, highlighting the urgent need for mechanisms that allow utility without sacrificing privacy. The central question the research tackles is whether it's possible to disclose only approximate regions for service functionality while completely hiding the exact, sensitive location.

To achieve this, the authors leverage the H3 geospatial indexing system developed by Uber. H3 is a hierarchical, global grid system that partitions the Earth's surface into hexagonal cells with unique indices. Its key advantages include the use of hexagons, which possess desirable geometric properties, minimal distortion compared to other systems, and support for various resolutions. This multi-resolution capability allows users to control the granularity of location obfuscation, balancing privacy with the required level of utility for a given application. The challenge, however, lies in converting high-precision latitude and longitude coordinates into H3 cell indices, a process that involves complex mathematical operations, including extensive trigonometric functions and handling very large and very small numbers. These operations traditionally pose a significant hurdle for accurate representation within the constraints of SNARK circuits.

A critical design decision in this work is the adoption of floating-point arithmetic over fixed-point arithmetic for calculations within the SNARKs. This choice is rooted in lessons learned from past computational disasters, such as the Arian 5 rocket explosion and the Intel Pentium FD bug, which underscored the paramount importance of accuracy and standard compliance in numerical computations. While fixed-point representations are simpler to implement in circuits, they struggle to accurately represent the wide dynamic range of numbers (from extremely small to extremely large) encountered in H3's geospatial calculations. As the authors demonstrate, fixed-point representations often achieve less accuracy, even when allocated more bits, making them unsuitable for the precision required for reliable geospatial indexing. Floating-point numbers, with their sign, exponent, and mantissa components, offer a more robust and standard-compliant way to approximate real numbers, thus ensuring the correctness and trustworthiness of the location obfuscation process within the zero-knowledge proof.

Key Findings

▶ Watch: Importance of floating-point arithmetic in SNARKs (2:00)

The research presents several significant contributions to the field of zero-knowledge proofs and location privacy:

1. Novel Floating-Point Gadget for SNARKs: The primary technical finding is the successful development and implementation of a new, highly accurate gadget for performing standard-compliant floating-point arithmetic within SNARK circuits. This gadget adheres to the IEEE 754 standard, addressing the long-standing challenge of representing and manipulating real numbers with sufficient precision in ZKP environments.
2. Zero-Knowledge Proof Circuit for H3 Algorithm: Building upon the floating-point gadget, the authors constructed a complete SNARK circuit that faithfully emulates the complex H3 algorithm. This circuit enables users to prove, in zero-knowledge, that a given approximate H3 cell index was correctly derived from their exact, private latitude and longitude coordinates, without revealing the exact coordinates themselves.
3. High Accuracy and Compatibility: Extensive evaluation demonstrated that their floating-point gadgets are fully compatible with the Berkeley TestFloat library, passing all generated test cases. Crucially, the full Zero-Knowledge Location Privacy (ZKLP) circuits, when using float64 precision, produced results entirely consistent ("all green") with the reference H3 implementation in C. In stark contrast, baseline circuits using fixed-point arithmetic, even with more bits, exhibited significant mismatches, validating the necessity and superiority of floating-point for this application.
4. Exceptional Efficiency and Performance: The developed circuits are remarkably efficient. The floating-point gadgets are compact, and their lookup constraints can be amortized, meaning the average cost per operation decreases with more operations. The overall ZKLP circuits boast significantly smaller circuit sizes and SRS (Structured Reference String) sizes, leading to low RAM usage. Furthermore, proof generation is fast, achievable even on low-end servers and mid-range mobile phones, making the solution practical for real-world deployment.
5. Practical Application in P2P Proximity Testing: The work demonstrates a concrete scenario where the ZKLP circuits can be effectively deployed: peer-to-peer proximity testing. In this application, a party can track their distance to up to 470 peers while preserving the privacy of their exact location, showcasing the scalability and utility of the proposed system.

Technical Deep Dive

▶ Watch: Construction of accurate floating-point SNARK circuits (2:50)

The technical core of this work lies in two main components: the construction of accurate floating-point arithmetic gadgets suitable for SNARKs, and the subsequent integration of these gadgets into a full zero-knowledge circuit for the H3 geospatial indexing algorithm.

Floating-Point Arithmetic Gadget Construction:

Floating-point numbers are crucial for approximating real numbers in computers, composed of a sign (s), an exponent (e), and a mantissa (m). For normal numbers, they represent a real value as (-1)^s m 2^e. The authors devised a four-step recipe for building SNARK gadgets for primitive floating-point operations:

1. Intermediate Value Computation: For any given operation (e.g., addition, multiplication), the gadget first computes intermediate sign, exponent, and mantissa values based on the specific arithmetic operation. This step involves standard floating-point logic, translated into circuit constraints.
2. Mantissa Normalization: The intermediate mantissa is then normalized to ensure its bit length matches the specified mantissa length m. This typically involves shifting the mantissa and adjusting the exponent accordingly, maintaining the numerical value.
3. Rounding: A critical step for accuracy, rounding ensures that the result conforms to the IEEE 754 standard. The default rounding rule, "round to nearest and ties to even," is implemented. This process is determined by three specific bits: a guard bit, a round bit, and a sticky bit, which capture information about the bits beyond the mantissa's precision. The gadget carefully computes and uses these bits to apply the correct rounding logic within the circuit.
4. Special Case Handling: Finally, the gadget includes logic to handle special floating-point cases, such as division by zero, overflow, underflow, and operations involving NaN (Not a Number) or infinity. This ensures robustness and compliance with the floating-point standard across all possible inputs.

ZLP Circuit Construction for H3:

With robust floating-point gadgets in place, the team proceeded to build the Zero-Knowledge Location Privacy (ZKLP) circuit by emulating the H3 algorithm. The H3 algorithm maps latitude and longitude coordinates to a unique hexagonal cell index. This process is described as "quite complicated," involving four main steps and numerous conversions among multiple coordinate systems (e.g., geographic to 3D Cartesian, then to 2D projection, and finally to H3 cell coordinates). A significant observation during this construction was the "huge number of trigonometric function computations" required, which are notoriously expensive to implement in SNARKs.

Circuit Optimizations:

To make the ZKLP circuits practical and efficient, several key optimizations were employed:

• Nondeterministic Advice (Hints): For computationally intensive operations like division, the circuit avoids emulating the full division logic. Instead, the prover is asked to provide the quotient Q and remainder R as "hints" or "nondeterministic advice." The circuit then only needs to verify the much simpler equality X = Q * Y + R, significantly reducing circuit size and proving time.
• Modified Floating-Point Representation:
• Avoiding Subnormal Numbers: Subnormal numbers (denormalized numbers) complicate floating-point arithmetic. The optimization allows the exponent to "underflow" to handle very small numbers without explicitly separating subnormal handling, simplifying the circuit.
• Removed Exponent Bias: Standard floating-point exponents are biased (a fixed value is added to the true exponent). Removing this bias in the circuit's internal representation can simplify exponent arithmetic.
• Explicit Leading One: For normal numbers, the leading bit of the mantissa is implicitly 1. Storing this "explicit leading one" can simplify certain bitwise operations and checks within the circuit.
• Lookup Arguments: These are used to minimize the cost of common circuit operations, particularly range checks (ensuring a value falls within a specific range) and power-of-2 computations. The authors further optimized by reducing the frequency of lookups. For instance, in right shift operations, a naive approach might require two lookups to check the range of the remainder. By first left-shifting the number, this can be reduced to a single lookup. This technique also applies to the rounding process of floating-point numbers.
• Elimination of Costly Trigonometric Functions: Recognizing the high cost of trigonometric functions (e.g., arcsin, tangent) in SNARKs, the researchers applied mathematical identities to remove many of them. For example, specific sigma identities were used to reformulate expressions. For the remaining trigonometric functions encountered during the computation of 2D coordinates, many could be precomputed outside the circuit, drastically reducing the in-circuit computational load.

These technical innovations and optimizations collectively enable the creation of a zero-knowledge proof system for location privacy that is both accurate and performant, addressing a significant gap in current privacy-preserving technologies.

Demo / Proof of Concept

▶ Watch: Evaluation results and performance of ZLP circuits (5:50)

The evaluation phase of the project focused on two critical aspects: compatibility with existing standards and implementations, and performance metrics.

Compatibility Testing:

1. Floating-Point Gadget Verification: The individual floating-point gadgets were rigorously tested against the Berkeley TestFloat library, a widely respected suite for verifying floating-point arithmetic implementations. The results were highly positive, with the developed gadgets passing "all of these tests," confirming their accuracy and compliance with the IEEE 754 standard.
2. ZKLP Circuit Verification against H3 C Implementation: The full Zero-Knowledge Location Privacy (ZKLP) circuits, designed to implement the H3 algorithm, were tested against Uber's reference H3 implementation in C. When configured to use float64 precision, the ZKLP circuits' outputs were "all green," meaning they were entirely consistent with the H3 C implementation. This critical finding validates that the complex geospatial calculations, including coordinate system conversions and trigonometric functions, are correctly and accurately replicated within the zero-knowledge environment.
3. Fixed-Point Baseline Comparison: To underscore the necessity of floating-point arithmetic, a baseline comparison was performed using fixed-point circuits. Even when fixed-point circuits were allocated "more bits than floating point," they consistently produced "mismatches" with the H3 C implementation. This stark contrast highlights the inherent limitations of fixed-point arithmetic for the wide dynamic range and precision requirements of geospatial computations and justifies the significant effort invested in accurate floating-point gadgets.

Performance Evaluation:

The performance of both the individual floating-point gadgets and the complete ZKLP circuits was thoroughly assessed:

• Floating-Point Gadgets: The gadgets themselves were found to be "quite small." A notable efficiency characteristic is that "part of the lookup constraints can be amortized," implying that with an increasing number of floating-point operations within a single proof, the average cost per operation decreases, making the solution more efficient for complex calculations.
• ZKLP Circuits: The full ZKLP circuits demonstrated "highly efficient" performance. They exhibited "much smaller circuit size" and "much smaller SRS size" compared to alternative approaches, directly translating to "low RAM usage" during proof generation and verification.
• Proof Generation Speed: The actual process of generating a zero-knowledge proof was "fast." This efficiency was observed "even on a low-end server as well as mid-range mobile phones," indicating the practical feasibility of deploying this privacy-preserving solution on resource-constrained devices.

Concrete Scenario: P2P Proximity Testing:

To illustrate a real-world application, the authors presented a scenario of peer-to-peer (P2P) proximity testing. In this setup, a party can privately determine their distance or proximity to a significant number of other parties. The evaluation showed that a single party "can track the distance to 470 peers" while preserving the privacy of their exact location coordinates. This demonstration highlights the scalability and utility of their ZKLP system for applications requiring private proximity queries, such as social networking, ride-sharing, or location-based gaming, without revealing sensitive precise locations.

Defensive Implications

▶ Watch: Limitations and future work on authentic location (7:00)

The development of accurate floating-point SNARKs for location privacy has profound implications for how individuals and organizations can protect sensitive location data. For defenders, the key takeaway is the practical viability of implementing zero-knowledge proofs as a robust mechanism for enforcing location privacy.

1. Embrace ZKP for Location-Based Services: Developers and service providers building location-based applications should seriously consider integrating ZKPs, such as the solution presented, to offer strong privacy guarantees to their users. Instead of collecting and storing precise user locations, applications can request proofs that a user's location falls within an approximate, privacy-preserving region (e.g., an H3 cell) for functionality, without ever learning the exact coordinates. This paradigm shift minimizes the risk of data breaches and misuse.
2. Leverage H3 for Obfuscation: The H3 framework by Uber is demonstrated as an effective and geometrically sound method for location obfuscation. Its multi-resolution capabilities allow applications to tailor the level of privacy (larger cells for more privacy, smaller for more utility) based on specific use cases and user preferences. Integrating H3 with ZKPs provides a powerful combination for verifiable, private location data.
3. Prioritize Numerical Accuracy: The research emphatically highlights the importance of accurate floating-point arithmetic in cryptographic circuits for geospatial data. Defenders should be wary of solutions that rely on less precise fixed-point arithmetic, especially for applications where even small errors can lead to privacy leaks or functional failures. The lessons from past computational disasters (Arian 5, Intel Pentium FD) serve as a stark reminder.
4. Addressing Location Authenticity: Acknowledging a limitation of the current work, which assumes the location being proven is authentic, the authors also point towards future defensive strategies. In many scenarios, such as C2PA (Coalition for Content Provenance and Authenticity) where a camera trustfully embeds an authentic location into a photo, the assumption holds. However, for broader applications, methods to cryptographically verify the authenticity of the reported location are crucial. Future work includes exploring solutions like leveraging "Find My" networks, cryptographically signed GPS signals, or TLS oracles to obtain verifiable and authentic location data before it enters the privacy-preserving ZKP pipeline. Defenders should monitor advancements in these areas to build end-to-end trustworthy location privacy systems.

By adopting these principles, organizations can transition from a "collect and protect" model to a "prove and use" model for location data, significantly enhancing user privacy and trust in location-based services.

Key Takeaways

• Zero-Knowledge Proofs for Location Privacy: The research demonstrates a practical and efficient method to achieve location privacy using SNARKs, allowing users to prove their location within an approximate region without revealing exact coordinates.
• H3 Framework for Obfuscation: Uber's H3 geospatial indexing system is effectively utilized for customizable location obfuscation, offering resolution control and geometric advantages for privacy-preserving applications.
• Accurate Floating-Point Arithmetic is Crucial: Standard-compliant floating-point arithmetic, implemented via novel SNARK gadgets, is essential for the precision required in geospatial calculations, outperforming fixed-point methods significantly.
• Highly Optimized and Efficient Circuits: The developed ZKLP circuits are small, use low RAM, and enable fast proof generation, even on mobile devices, making them suitable for real-world deployment.
• Real-World Applicability: The system supports practical scenarios like P2P proximity testing, allowing private distance tracking for up to 470 peers.
• Future Focus on Location Authenticity: While current work assumes authentic location, future efforts will integrate mechanisms like signed GPS or TLS oracles to establish the trustworthiness of the initial location input.

About the Speaker(s)

The work "Zero-Knowledge Location Privacy via Accurate Floating-Point SNARKs" was presented by Chengru Zhang. Chengru Zhang is a co-author of this research, which is a joint effort with Jens Ernstberger, Luca Ciprian, Philipp Jovanovic, and Sebastian Steinhorst. While specific titles and affiliations for each individual are not detailed in the transcript, the metadata indicates that these researchers are affiliated with institutions, and their collective expertise spans the fields of zero-knowledge proofs, cryptography, and embedded systems, contributing to this significant advancement in privacy-preserving technologies.