Blockchain Papers

Danslav Slavenskoj, Lingenic LLC

Introduction The processing of Unicode text is among the most foundational operations in modern computing, yet the algorithms that govern it—segmentation, normalization, bidirectional layout, collation—are specified across more than a dozen Unicode Technical Annexes and Reports, each encoding rules of considerable complexity. Implementations of these algorithms in widely used libraries have historically been written in memory-unsafe languages without formal guarantees, relying on testing alone to establish correctness. The question of whether a Unicode text processing library can be not merely tested but proved correct—with machine-checked guarantees of both the absence of runtime errors and functional conformance to the Unicode Standard—has not, to the authors' knowledge, been addressed prior to this work. Lingenic-Text is a complete implementation of the Unicode 17.0 text processing stack, written in SPARK/Ada (Ada 2022) and formally verified with GNATprove. The library comprises approximately 32,200 lines of Ada source across 57 files, implementing fourteen distinct modules: UTF-8 encoding and decoding (RFC 3629), grapheme cluster segmentation, word segmentation, and sentence segmentation (UAX #29), line breaking (UAX #14), normalization to all four forms (UAX #15), case mapping including full multi-character mappings and context-sensitive rules (Unicode §3.13), collation with DUCET support (UTS #10), the full Unicode Bidirectional Algorithm including bracket pair resolution (UAX #9), East Asian width determination (UAX #11), emoji classification and property lookup (UTS #51), identifier detection (UAX #31), and internationalized domain name processing with Punycode (UTS #46, RFC 3492). Every verification condition—9,640 in total, spanning runtime checks, functional contracts, assertions, termination, initialization, and data dependencies—is discharged by the prover at Level 4. No pragma Assume appears anywhere in the codebase. Conformance testing against Unicode Consortium test suites and reference data passes all 504,634 test cases. Architecture and Verification Approach The verification architecture factors into two links of different strength. The first link is a formal proof: for every subprogram in the library, a ghost specification encodes the intended behavior as pure expression functions or recursive ghost functions, and GNATprove proves that the implementation satisfies this specification for all possible inputs. This link is machine-checked and universal. Ghost code in SPARK is erased entirely at compile time, imposing zero runtime cost. The second link is conformance testing against the Unicode Consortium test suites—GraphemeBreakTest.txt, NormalizationTest.txt, BidiCharacterTest.txt, and others—which validates that the ghost specifications themselves faithfully encode the rules of the Unicode Standard. This link is empirical: it is validation by examples, and its strength is bounded by the coverage of the test suites. The end-to-end guarantee is therefore proved(implementation ⊨ specification) ∧ tested(specification ≈ standard). Along the implementation-correctness axis, the guarantee is a proof; along the standard-conformance axis, it is only as strong as the test suite. Since the Unicode Standard is a natural-language document, the conformance boundary cannot be eliminated by formal methods alone, but the test suites are the Consortium's own conformance instruments, and the library passes all 504,634 cases. Two principal proof patterns emerge across the library's modules. In the first, used by the segmentation algorithms, the Unicode rules are encoded as a recursive ghost function with a Subprogram_Variant annotation proving termination. The implementation is a forward state machine realized as a loop, whose invariant asserts equivalence with the recursive specification at every iteration. The postcondition of the public subprogram then states that its output equals the value of the recursive ghost function applied to the input. In the second pattern, used by normalization and case mapping, a generic text transformation framework carries a ghost predicate (Partial_Valid) as its loop invariant. Each callback's postcondition preserves this invariant, and a finishing postcondition bridges from the partial invariant to the full output specification. This generic is instantiated by each module with its own callback and specification, yielding proved correctness without duplicating the proof scaffolding. All property lookups—script, general category, grapheme break property, word break, sentence break, line break, East Asian width, Bidi class, joining type, and others—are implemented as flat arrays indexed directly by codepoint, giving O(1) access with no dynamic allocation, no hash tables, and no trees. The Unicode Character Database files are read from disk at initialization by a proved UCD parser, whose postcondition guarantees that every codepoint's property value in the populated table matches the value specified by a recursive ghost function encoding a model of the UAX #44 property file format. The fidelity of that model to the actual UAX #44 text is, like the algorithm specifications, established by test rather than by proof. This design permits updating to a new Unicode version by replacing the data files in the ucd/ directory, without modifying any source code. Scope and Capabilities The library provides a complete C API as a static library with 53 exported functions, enabling integration with C, C++, and any language supporting C foreign function interfaces. The C binding is a thin validation layer: every entry point checks its arguments against the precondition of the proved SPARK subprogram it wraps, returning an error code on violation, so that the machine-checked postconditions of the core apply to every successful call through the C interface. Among the more complex modules, the Bidirectional Algorithm implementation handles the full rule set of UAX #9, including explicit embeddings, overrides, and isolates, isolating run sequence resolution, and bracket pair matching under rule N0 with the BD16 algorithm. The reordering procedure produces a proved permutation of the input. The collation module implements UTS #10 with both Non-Ignorable and Shifted variable weighting, contraction handling, and implicit weight computation for CJK Unified Ideographs, Tangut, Nushu, and Khitan Small Script. The IDNA module implements the full UTS #46 processing pipeline with Punycode encoding (RFC 3492), ContextJ validation (RFC 5892), Bidi domain name rules (RFC 5893), and DNS length checks. The library enforces several invariants by construction. No heap allocation occurs; all buffers are bounded arrays with every index proved in range, eliminating buffer overflows as a class of defect. No runtime exceptions are raised; all error conditions are communicated through status codes. Runtime checks are suppressed in the compiled binary (-gnatp) because GNATprove has already proved their absence. The sole code outside SPARK verification is the file I/O routine that reads UCD data from disk; every other subprogram is machine-checked. Availability Lingenic-Text version 1.2.0 implements Unicode Standard 17.0. The source code, comprising all SPARK/Ada sources, the C binding, and conformance test programs, is available under the Lingenic Source-Available License v2.3. Production use requires a separate license from Lingenic LLC. The Unicode Character Database files included in the distribution are © Unicode, Inc. and are distributed under the Unicode License V3.

Tarunesh Verma, Yichao Yuan, Nishil Talati, Todd Austin

Zero-Knowledge Proofs (ZKP) are protocols which construct cryptographic proofs to demonstrate knowledge of a secret input in a computation without revealing any information about the secret. ZKPs enable novel applications in private and verifiable computing such as anonymized cryptocurrencies and blockchain scaling and have seen adoption in several real-world systems. Prior work has accelerated ZKPs on GPUs by leveraging the inherent parallelism in core computation kernels like Multi-Scalar Multiplication (MSM). However, we find that a systematic characterization of execution bottlenecks in ZKPs, as well as their scalability on modern GPU architectures, is missing in the literature. This paper presents ZKProphet, a comprehensive performance study of Zero-Knowledge Proofs on GPUs. Following massive speedups of MSM, we find that ZKPs are bottlenecked by kernels like Number-Theoretic Transform (NTT), as they account for up to 90% of the proof generation latency on GPUs when paired with optimized MSM implementations. Available NTT implementations under-utilize GPU compute resources and often do not employ architectural features like asynchronous compute and memory operations. We observe that the arithmetic operations underlying ZKPs execute exclusively on the GPU's 32-bit integer pipeline and exhibit limited instruction-level parallelism due to data dependencies. Their performance is thus limited by the available integer compute units. While one way to scale the performance of ZKPs is adding more compute units, we discuss how runtime parameter tuning for optimizations like precomputed inputs and alternative data representations can extract additional speedup. With this work, we provide the ZKP community a roadmap to scale performance on GPUs and construct definitive GPU-accelerated ZKPs for their application requirements and available hardware resources.

Hinata Nishino, Kazumasa Omote, Keita Emura

Nominative signatures allow us to indicate who can verify a signature, and they can be employed to construct a non-transferable signature verification system that prevents the signature verification by a third party in unexpected situations. For example, this system can prevent IOU/loan certificate verification in unexpected situations. However, nominative signatures themselves do not allow the verifier to check whether the funds will be transferred in the future or have been transferred.It would be desirable to verify the fact simultaneously when the system involves a certain money transfer such as cryptocurrencies/cryptoassets. In this paper, we propose a smart contract-based non-transferable signature verification system using nominative signatures. We pay attention to the fact that the invisibility, which is a security requirement to be held for nominative signatures, allows us to publish nominative signatures on the blockchain. Our system can verify whether a money transfer actually will take place, in addition to indicating who can verify a signature. We transform the Hanaoka-Schuldt nominative signature scheme (ACNS 2011, IEICE Trans. 2016) which is constructed over a symmetric pairing to a scheme constructed over an asymmetric pairing, and evaluate the gas cost when a smart contract runs the verification algorithm of the modified Hanaoka-Schuldt nominative signature scheme.

Ruiteng Zhang, Pingbin Luo, Qiong Huang

No abstract is available for this record.

Soumya Bhoumik, Sarbari Mitra, Rohit Sharma, Kuldeep Namdeo

Identity-based cryptography (IBC), proposed by Adi Shamir, revolutionized public key authentication by eliminating the need for certificates, enabling a more efficient and scalable approach to cryptographic systems. Meanwhile, in \cite{Katsumata2024group}, Katsumata et al. were the first to present the blind signature protocol based on the hardness assumption of isogeny with provable security, which resembles the Schnorr blind signature. Building upon these foundational concepts, we propose an Identity-Based Blind Signature Scheme with an Honest Zero-Knowledge Verifier utilizing the CSIDH framework. This scheme combines blind signatures for privacy preservation with zero-knowledge proofs to ensure the verifier's honesty without revealing any additional information. Leveraging the quantum-resistant properties of CSIDH, a post-quantum secure scheme based on supersingular isogenies, our scheme offers strong protection against quantum adversaries while maintaining computational efficiency. We analyze the security of the introduced protocol in the standard cryptographic model and demonstrate its effectiveness in safeguarding privacy and verifier honesty. Furthermore, we present a performance evaluation, confirming the practical viability of this quantum-resistant cryptographic solution for privacy-preserving applications. This work advances the creation of secure, and scalable cryptographic systems for the post-quantum era.

Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olšák · 6 authors

The development of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is therefore to make use of SAT solvers in expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is synthesizing the appropriate instances from the typically infinite Herbrand universe. In this work, we develop a machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on a graph neural network (GNN) that learns from problems and their solutions independently of many symmetries and symbol names (addressing the abundance of Skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then combined with an efficient ground solver and, starting with zero knowledge, iteratively trained on a large corpus of mathematical problems. We show that the system is capable of solving many problems by such educated guessing, finding proofs for 32.12% of the training set. The final trained system solves 19.74% of the unseen test data on its own. We also observe that the trained system finds solutions that the iProver and CVC5 systems did not find.

Worasait Suwannik

Multiple sequence alignment (MSA) is a fundamental algorithm in bioinformatics. In a situation when the alignment might need to be protected while revealing the other information such the input sequences and the alignment score, zero knowledge proof can be used. In this paper, a validator checks the consistency between the input sequence and the alignment, and between the alignment and the alignment score. The validator is written in Circom language which will be compile into a circuit. Using a zero knowledge prove system called zkSNARK, a cryptographic proof is generates for the circuit and its input. This proof demonstrates that all inputs are consistent without revealing the actual alignment.

Shuxun Wang, Yunfei Lei, Ziqi Zhang, Wei Liu · 10 authors

With the rise of "Metaverse" and "Web 3.0", Non-Fungible Token (NFT) has emerged as a kind of pivotal digital asset, garnering significant attention. By the end of March 2024, more than 1.7 billion NFTs have been minted across various blockchain platforms. To effectively locate a desired NFT, conducting searches within a vast array of NFTs is essential. The challenge in NFT retrieval is heightened due to the high degree of similarity among different NFTs, regarding regional and semantic aspects. In this paper, we will introduce a benchmark dataset named "NFT Top1000 Visual-Text Dataset" (NFT1000), containing 7.56 million image-text pairs, and being collected from 1000 most famous PFP1 NFT collections2 by sales volume on the Ethereum blockchain. Based on this dataset and leveraging the CLIP series of pre-trained models as our foundation, we propose the dynamic masking fine-tuning scheme. This innovative approach results in a 7.4\% improvement in the top1 accuracy rate, while utilizing merely 13\% of the total training data (0.79 million vs. 6.1 million). We also propose a robust metric Comprehensive Variance Index (CVI) to assess the similarity and retrieval difficulty of visual-text pairs data. The dataset will be released as an open-source resource. For more details, please refer to: https://github.com/ShuxunoO/NFT-Net.git.

Nawras H. Sabbry, Алла Левина

<abstract> <p>This paper proposes a deterministic nonce generation technique to address the catastrophic issues associated with nonce reuse in message signing and to enhance the efficiency of Schnorr multi-signature schemes. Additionally, this research aims to reduce computational complexity and bandwidth requirements in digital and multi-signature schemes while maintaining robust security against common attacks. The proposed method was inspired by the EdDSA approach. The methodology includes a comprehensive mathematical analysis of digital signature algorithms and a rigorous examination of their vulnerabilities to well-known cryptographic attacks. This analysis evaluates the effectiveness and robustness of the proposed nonce generation technique within the frameworks of the Schnorr digital signature and the two-round MuSig schemes. Techniques and tools employed in this research involve deterministically generating nonces by hashing the private key and subsequently hashing the result with the message. Furthermore, it is proposed to exclude the public nonce R from the challenge calculations and to allow signers to directly prove possession of their secret keys through the aggregated public key, thereby eliminating the need for non-interactive zero-knowledge (NIZK) proofs. The findings demonstrate significant reductions in computational complexity and operational requirements, thereby improving bandwidth efficiency and making this method well-suited for resource-constrained devices. The approach also exhibits strong resistance to various attacks, including nonce reuse, key cancellation, rogue keys, and virtual machine rewinding.</p> </abstract>

Sahil Wadhwani

Abstract: Certificates help students not only to prove their achieved goals and milestones but also ensure that he/she maintains a high level of knowledge in that particular field. An estimated total of 25.57 crore Indian students have been enrolled for primary to higher education in 2020–21 and nearly 65 lakhs of them graduate each year. Throughout this journey, a student generates a myriad number of certificates that may include results, transcripts, degrees, diplomas, etc. A student has to submit these certificates to apply for a job or seek higher admission in any particular organization. A major problem today is manually verifying and authenticating these certificates. Many hardworking people with genuine certificates get rejected and suffer because of the lack of a system that can differentiate original certificates from fake ones. With easy access to cheap and advanced software, document forgery has become a matter of concern nowadays. This scenario demands an updated system that could not only store documents safely but also help verify and authenticate them, their issuers, and holders in a way that is much simpler, effective, and secure. Blockchain technology comes up as a solution to all these problems. Blockchain has recently emerged as a potential means for the document-authentication process and can be easily used to tackle document forgery and counterfeiting as it follows a decentralized approach. Our proposed model includes several methods such as unique hash generation, key cryptography, digital ledgers, proof of work, digital signatures, and distributed storage which has made the document-verification process easier and more secure for both the certificate-generating organization and the holder of the certificate. The SHA-256 algorithm has been used to assign a unique hash to each uploaded document which can be used to validate its authenticity. Thus, this system meets up all the criteria for a document verification system by overcoming the drawbacks and difficulties currently faced in the traditional methods of document verification.