Costly synchronous write-a.k.a., fsync()-is a common approach to preserve the storage order of data. Android smartphones use No-Barrier by default to improve fsync() performance. Recently, Barrier-Enabled IO Stack (BEIOS) provides an efficient order-preserving method for flash storage by barrier write commands (BWCs). However, our evaluation shows that BEIOS suffers from performance degradation in multi-threaded scenarios since BWCs increase linearly with the number of threads. This paper proposes LazyBarrier, a new order-preserving IO stack mainly involving orderpreserving write (OPW) Model, the Lazy Issue algorithm, modified F2FS, and Barrier Scheduling. OPW Model is based on Finite Automata and defines state transition in OPW. Lazy Issue is a novel algorithm that minimizes BWCs. F2FS is modified to support OPW, and Barrier Scheduling solves the ordering problem in multi-queue block layer. The experiments on Android smartphones show that, compared with BEIOS, LazyBarrier improves OPW performance by 73% and 29% under the FIO benchmark and in real applications respectively. And LazyBarrier also outperforms BEIOS by 19% in dbench workload in servers.

We propose an I/O stack for ZNS based flash storage in mobile environment, ZMS, The zone interface is known to save the flash storage from two fundamental issues which modern flash storage suffers from; logical-to-physical mapping table size and garbage collection overhead. Through extensive study, we find that realizing the zone interface in mobile environment is more than a challenge due to the unique characteristics of mobile environment: the lack of on-device memory in mobile flash storage and the frequent f sync 1) calls in mobile applications. Aligned with this, we identify the root causes that need to he addressed in realizing the zone interface in mobile I/O stack: write buffer thrashing and tiny synchronous file update. We develop a filesystem, block I/O layer, and device firmwarc techniques to address the above mentioned two issues. The three key techniques in ZMS are (i) (ii) budget-based in-place update, and (iii) multi-granularity logical-to-physical mapping. Evaluation on a real production platform shows that ZMS improves write amplification by 2.9-6.4x and random write performance by 5,0-13,6x, With the three techniques, ZMS shows significant performance improvement in writing to the multiple zones concurrently, executing SQLite transactions, and launching the. applications.

User applications that require transactional file access generally use user-level transactional protocols such as logging, atomic rename, since the POSIX interface does not support transactional file operations. The user-level protocols are complex and require specific persistence properties of file systems for correctness. If the kernel provides transactional access to file data, application developers can avoid the complex and error-prone application-level protocols. Many previous studies on kernel-level transactional support have several critical limitations such as complex APIs, file system-dependence, and low transaction concurrency. In this paper, we propose a kernel-level write-ahead logging (WAL) technique, called KWAL. KWAL maintains user-transparent WAL files and redirects transactional IOs to them. Since KWAL is implemented as a stackable file system, it can be mounted over any native file systems, without modifying them. To provide a higher transaction concurrency while guaranteeing isolation, KWAL supports byte-level write conflict detection and repeatable read isolation. We also utilize a block remap technique to resolve the duplicate write problem of WAL-based transaction scheme. To demonstrate the usefulness of KWAL, we implemented a simple key-value store using KWAL APIs, fixed the wrong transaction implementation of the Git application, and simplified the implementation of the storage engines of MySQL and SQLite.

Interactive proofs are a type of verifiable computing that secures the integrity of computations. The need is increasing as more computations are outsourced to untrusted parties, e.g., cloud computing platforms. Existing techniques, however, have mainly focused on exact computations, but not approximate arithmetic (e.g., floating-point or fixed-point arithmetic). This makes it hard to apply them to certain types of computations (e.g., machine learning or financial applications) that inherently require approximate arithmetic. In this paper, we present an efficient interactive proof system for arithmetic circuits with rounding gates that can represent approximate arithmetic. The main idea is to reduce the rounding gate into a small sub-circuit without rounding, and reuse the machinery of the Goldwasser, Kalai, and Rothblum’s protocol (also known as the GKR protocol) and its recent refinements. Specifically, we shift the algebraic structure from a field to a ring to better deal with the notion of “digits”, and generalize the original GKR protocol over a ring. Then, we reduce the rounding operation to a low-degree polynomial over a ring, and develop a novel, optimal circuit construction of an arbitrary polynomial to transform the rounding polynomial to an optimal circuit representation. Moreover, further optimization on the proof generation cost for rounding is presented employing a Galois ring. Our experimental results show the efficiency of our protocol for approximate arithmetic, e.g., the implementation performed two orders of magnitude better than the existing system for a nested 128 by 128 matrix multiplication of depth 12 on the 16-bit fixed-point arithmetic.

We propose a new design for a Translation Validation (TV) system geared towards practical use with modern optimizing compilers, such as LLVM. Unlike existing TV systems, which are custom-tailored for a particular sequence of transformations and a specific, common language for input and output programs, our design clearly separates the transformation-specific components from the rest of the system, and generalizes the transformation-independent components. Specifically, we present Keq, the first program equivalence checker that is parametric to the input and output language semantics and has no dependence on the transformation between the input and output programs. The Keq algorithm is based on a rigorous formalization, namely cut-bisimulation, and is proven correct. We have prototyped a TV system for the Instruction Selection pass of LLVM, being able to automatically prove equivalence for translations from LLVM IR to the MachineIR used in compiling to x86-64. This transformation uses different input and output languages, and as such has not been previously addressed by the state of the art. An experimental evaluation shows that Keq successfully proves correct the translation of over 90% of 4732 supported functions in GCC from SPEC 2006.

We report our experience in the formal verification of the deposit smart contract, whose correctness is critical for the security of Ethereum 2.0, a new Proof-of-Stake protocol for the Ethereum blockchain. The deposit contract implements an incremental Merkle tree algorithm whose correctness is highly nontrivial, and had not been proved before. We have verified the correctness of the compiled bytecode of the deposit contract to avoid the need to trust the underlying compiler. We found several critical issues of the deposit contract during the verification process, some of which were due to subtle hidden bugs of the compiler.

We propose an algorithmic semantics-based approach for proving equivalence of programs written in possibly different languages. We introduce a new notion of bisimulation, named cut-bisimulation, that allows the two programs to semantically synchronize at relevant “cut” points, but to evolve independently otherwise. While being analogous, cut-bisimulation is different from stuttering bisimulation. We provide realistic counter-example programs that are cut-bisimilar but not stuttering-bisimilar, which can be easily found in a compiler optimization. Also, we identify a subclass of stuttering bisimulation that can be reduced to cut-bisimulation. Based on cut-bisimulation, we have implemented the first language-independent tool for proving program equivalence, parametric in the formal semantics of the source and target languages, built on top of the K framework. As a preliminary evaluation, we instantiated our tool with an LLVM semantics, and used it to prove equivalence of the aforementioned example programs written in LLVM.

We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs. This work is an extended version of a conference paper titled “Invariant Synthesis for Incomplete Verification Engines”.

We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite. This extensive testing paid off, revealing bugs in both the x86-64 reference manual and other existing semantics. We also illustrate potential applications of our semantics in different formal analyses, and discuss how it can be useful for processor verification.

대부분의 시스템에서 데이터 내구성을 보장하기 위해 fsync 시스템 콜을 사용한다. fsync 시스템 콜은 현재 수행 중인 프로세스와 동기적으로 동작하기 때문에 fsync 시스템 콜의 지연시간을 개선하는 것은 시스템의 응답시간 측면에서 중요하다. 기존의 컴파운드 트랜잭션으로 인한 fsync 시스템 콜의 지연시간을 파일 수준 저널링을 사용하여 개선한 연구가 있으나 짧은 시기에 여러 코어에서 fsync 시스템콜이 발생할 경우 컴파운드 트랜잭션에 비해서 플러시 명령 횟수가 증가한다. 따라서 본 논문에서는 파일수준 저널링에서 플러시 명령 횟수 증가로 인한 fsync 지연시간 문제를 해결하기 위해 짧은 시기에 여러 코어에서 발생한 fsync 시스템 콜들을 한꺼번에 묶어서 처리하는 fsync 병합 기법을 제안한다.

Machine learning on (homomorphic) encrypted data is a cryptographic method for analyzing private and/or sensitive data while keeping privacy. In the training phase, it takes as input an encrypted training data and outputs an encrypted model without ever decrypting. In the prediction phase, it uses the encrypted model to predict results on new encrypted data. In each phase, no decryption key is needed, and thus the data privacy is ultimately guaranteed. It has many applications in various areas such as finance, education, genomics, and medical field that have sensitive private data. While several studies have been reported on the prediction phase, few studies have been conducted on the training phase.In this paper, we present an efficient algorithm for logistic regression on homomorphic encrypted data, and evaluate our algorithm on real financial data consisting of 422,108 samples over 200 features. Our experiment shows that an encrypted model with a sufficient Kolmogorov Smirnow statistic value can be obtained in ∼17 hours in a single machine. We also evaluate our algorithm on the public MNIST dataset, and it takes ∼2 hours to learn an encrypted model with 96.4% accuracy. Considering the inefficiency of homomorphic encryption, our result is encouraging and demonstrates the practical feasibility of the logistic regression training on large encrypted data, for the first time to the best of our knowledge.

Verifiable computing (VC) is a complexity-theoretic method to secure the integrity of computations. The need is increasing as more computations are outsourced to untrusted parties, e.g., cloud platforms. Existing techniques, however, only deal with exact computations, without the capability of rounding (e.g., “1.11 × 2.22 = 2.4642” is verifiable, but “1.11 × 2.22 rounds-to 2.46” is not). Hence, in a long sequence of calculations (e.g., multiplications), the number of digits of the result keeps increasing and will quickly exceed the precision limit of the underlying system. Because of this limitation, VC is currently missing the opportunity in the whole AI space where approximate computations are unavoidable. In pursuit of the vision of verifiable AI computing, a solution to support the rounding operation is necessary. In this paper, we present an efficient verifiable computing scheme to achieve it. The main idea is to reduce the rounding operation into an efficient arithmetic circuit representation, and reuse the machinery of the Goldwasser, Kalai, and Rothblum’s protocol (also known as the GRK protocol), the state-of-the-art interactive proof protocol. Specifically, we shift the algebraic structure from a field to a ring to better deal with the notion of “digits”, and generalize the original GKR protocol over a ring. Then, we reduce the rounding operation to a low-degree polynomial in a ring, and present a novel, optimal circuit construction of an arbitrary polynomial to transform the rounding polynomial to an optimal arithmetic circuit representation. Moreover, we further optimize the proof generation cost for rounding by employing a Galois ring. We provide experimental results that show the efficiency of our scheme for approximate computations. For example, our implementation performed two orders of magnitude better than the existing GKR protocol for a nested 128×128 matrix multiplication of depth 12 on the 16-bit fixed-point arithmetic.

In this paper, we introduce a new color filter array interpolation based on edge map prediction using the Bayesian theorem. The edge information obtained at the position of the green component sampled in the quincunx grid using the Bayer pattern is used to predict the edge of the red and blue component positions distributed in the rectangular grid. In this process, the edge distribution of the entire image, local area, and nearest neighbors is analyzed to determine the smooth/edge characteristics stochastically. If the pixels at the red and blue positions are determined to be edge pixels, the edge direction is inherited from the edge pixels of the local region. By combining a new decision technique with directional weighted interpolation in the green plane reconstruction process, the interpolation accuracy can be improved compared with the existing demosaicking algorithms. After interpolating the green channel, the color difference between the interpolated green channel and the red/blue channel is used to refine the reconstructed green plane. The other color planes can then be interpolated using this refined green plane. Experimental results show that our algorithm improves both the objective and subjective image qualities compared with the conventional state-of-the-art demosaicking algorithms.

We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.

A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions. Unfortunately, the rise of these technologies has been marred by a series of costly bugs and exploits. Increasingly, the Ethereum community has turned to formal methods and rigorous program analysis tools. This trend holds great promise due to the relative simplicity of smart contracts and bounded-time deterministic execution inherent to the Ethereum Virtual Machine (EVM). Here we present KEVM, an executable formal specification of the EVM's bytecode stack-based language built with the K Framework, designed to serve as a solid foundation for further formal analyses. We empirically evaluate the correctness and performance of KEVM using the official Ethereum test suite. To demonstrate the usability, several extensions of the semantics are presented. and two different-language implementations of the ERC20 Standard Token are verified against the ERC20 specification. These results are encouraging for the executable semantics approach to language prototyping and specification.

In this paper, we introduce a weighted sum-based color filter array interpolation method using Taylor series cubic approximation. We use a high-order approximation to predict accurate pixel values during the reconstruction of quincunx grid-sampled green channels, and perform a weighted average-based interpolation in a large local window. We also perform prediction utilizing a color difference model in a small local window to generate additional green values. By applying the weighted sum method to the predicted green values in two local windows, green channel can be enhanced. The remaining color components, namely, the rectangular grid-sampled red and blue channels, are interpolated utilizing the weighted average method of the color difference model. Additionally, we propose a post-processing method that removes the zipper artifacts generated during the interpolation process. Experimental results demonstrate that the proposed color filter array interpolation system outperforms existing algorithms in terms of both objective and subjective performance.

In this paper, we propose a new demosaicking system that uses post-processing technique to remove zipper artifacts that are primarily caused by improper interpolation in a quincunx-sampled green plane. We use a high-order approximation to predict accurate pixel values in the weighted average-based green channel interpolation. We also perform prediction using a color difference model in the red and blue channel interpolation process. As a well-designed demosaicking system too cannot prevent the occurrence of ON-OFF pattern artifacts and the resulting false colors, we propose post-processing for zipper artifact detection and removal to improve the demosaicked image. After performing the just noticeable difference modelbased zipper artifact detection in the luminance image of the demosaicked image, the clamping-based zipper artifact removal process is performed in the red, green, and blue planes. Experimental results demonstrate that the proposed demosaicking system improves both the objective and subjective image qualities compared to the conventional state-of-the-art demosaicking algorithms.