arXiv subjects

Bow-Yaw Wang

Publications and source records attributed to Bow-Yaw Wang.

11 recordsLinked to original sources

arXiv2026

Synthesizing Probabilistic Saturating Counters with Differentially Private Formal Guarantees

Branch predictors improve instruction-level parallelism in modern processors and are commonly modeled using saturating counters. However, classical saturating counters are deterministic and thus vulnerable to side-channel attacks: an attacker can manipulate the counter state and infer the branch direction of a victim process. Probabilistic saturating counters (PSCs) have been proposed to mitigate this leakage by randomizing counter updates, but existing evaluations are mainly empirical. In this paper, we give a formal analysis based on differential privacy (DP): we model PSCs and the corresponding Prime+Probe attack strategies as probabilistic Moore machines, derive optimal attack strategies, and quantify the attacker's distinguishing power through DP. Our DP guarantee applies to the PSC primitive under the Prime+Probe observation model; end-to-end security for a full branch predictor under repeated or adaptive attacks is an important direction for future work. We then synthesize parameters for an enhanced PSC that satisfies a target pure DP guarantee. To evaluate utility, we derive the stationary misprediction rate and validate the theoretical predictions on benchmark programs. Compared to deterministic and existing probabilistic saturating counters, the synthesized PSCs provide formal security guarantees while preserving competitive prediction performance.

cs.CR↗

arXiv2026

SAT-Solving the Poset Cover Problem

The poset cover problem seeks a minimum set of partial orders whose linear extensions cover a given set of linear orders. Recognizing its NP-completeness, we devised a non-trivial reduction to the Boolean satisfiability problem using a technique we call swap graphs, which avoids the complexity explosion of the naive method. By leveraging modern SAT solvers, we efficiently solve instances with reasonable universe sizes. Experimental results using the Z3 theorem prover on randomly generated inputs demonstrate the effectiveness of our method.

cs.LO↗

arXiv2025

Quantitative Auditing of AI Fairness with Differentially Private Synthetic Data

Fairness auditing of AI systems can identify and quantify biases. However, traditional auditing using real-world data raises security and privacy concerns. It exposes auditors to security risks as they become custodians of sensitive information and targets for cyberattacks. Privacy risks arise even without direct breaches, as data analyses can inadvertently expose confidential information. To address these, we propose a framework that leverages differentially private synthetic data to audit the fairness of AI systems. By applying privacy-preserving mechanisms, it generates synthetic data that mirrors the statistical properties of the original dataset while ensuring privacy. This method balances the goal of rigorous fairness auditing and the need for strong privacy protections. Through experiments on real datasets like Adult, COMPAS, and Diabetes, we compare fairness metrics of synthetic and real data. By analyzing the alignment and discrepancies between these metrics, we assess the capacity of synthetic data to preserve the fairness properties of real data. Our results demonstrate the framework's ability to enable meaningful fairness evaluations while safeguarding sensitive information, proving its applicability across critical and sensitive domains.

cs.CY↗

arXiv2024

Ensuring Fairness with Transparent Auditing of Quantitative Bias in AI Systems

With the rapid advancement of AI, there is a growing trend to integrate AI into decision-making processes. However, AI systems may exhibit biases that lead decision-makers to draw unfair conclusions. Notably, the COMPAS system used in the American justice system to evaluate recidivism was found to favor racial majority groups; specifically, it violates a fairness standard called equalized odds. Various measures have been proposed to assess AI fairness. We present a framework for auditing AI fairness, involving third-party auditors and AI system providers, and we have created a tool to facilitate systematic examination of AI systems. The tool is open-sourced and publicly available. Unlike traditional AI systems, we advocate a transparent white-box and statistics-based approach. It can be utilized by third-party auditors, AI developers, or the general public for reference when judging the fairness criterion of AI systems.

cs.CY↗

arXiv2022

Analyzing FreeRTOS Scheduling Behaviors with the Spin Model Checker

FreeRTOS is a real-time operating system with configurable scheduling policies. Its portability and configurability make FreeRTOS one of the most popular real-time operating systems for embedded devices. We formally analyze the FreeRTOS scheduler on ARM Cortex-M4 processor in this work. Specifically, we build a formal model for the FreeRTOS ARM Cortex-M4 port and apply model checking to find errors in our models for FreeRTOS example applications. Intriguingly, several errors are found in our application models under different scheduling policies. In order to confirm our findings, we modify application programs distributed by FreeRTOS and reproduce assertion failures on the STM32F429I-DISC1 board.

cs.FL↗

arXiv2022

Defensive Design of Saturating Counters Based on Differential Privacy

The saturating counter is the basic module of the dynamic branch predictor, which involves the core technique to improve instruction level parallelism performance in modern processors. However, most studies focus on the performance improvement and hardware consumption of saturating counters, while ignoring the security problems they may cause. In this paper, we creatively propose to study and design saturating counters from the defense perspective of differential privacy, so that attackers cannot distinguish the states that saturating counters are in and further infer sensitive information. To obtain theoretical guarantees, we use Markov chain to formalize the attack algorithm applied to the saturating counter, investigate into the optimal attack strategy and calculate the probability of successful attack. Furthermore, we find that the attacker is able to accurately guess the branch execution of the victim's process in the existing saturating counters. To avoid this, we design a new probabilistic saturating counter, which generalizes the existing conventional and probabilistic saturating counters. The guarantee of differential privacy is applied to deduce parameters of the new saturating counters so that the security requirement can be satisfied. We also theoretically calculate the misprediction rate when the saturating counter reaches the steady state. The experimental results on testing programs show that the calculated theoretical results agree with the experimental performances. Compared with the existing conventional and probabilistic saturating counters, when the parameters of our designed models are selected appropriately, the new saturating counters can not only ensure similar operational performance, but also establish strict security guarantee.

cs.CR↗

arXiv2018

A Spin-based model checking for the simple concurrent program on a preemptive RTOS

We adapt an existing preemptive scheduling model of RTOS kernel by eChronos from machine-assisted proof to Spin-based model checker. The model we constructed can be automatically verified rather than formulating proofs by hand. Moreover, we look into the designs of a Linux-like real-time kernel--Piko/RT and the specification of ARMv7-M architecture to reconstruct the model, and use LTL to specify a simple concurrent programs--consumer/producer problem during the development stage of the kernel. We show that under the preemptive scheduling and the mechanism of ARMv7-M, the program will not suffer from race condition, starvation, and deadlock.

cs.OS↗

arXiv2017

An Executable Sequential Specification for Spark Aggregation

Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs.

cs.DC↗

arXiv2015

PAC Learning-Based Verification and Model Synthesis

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.

cs.SE↗

arXiv2015

Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

We apply multivariate Lagrange interpolation to synthesize polynomial quantitative loop invariants for probabilistic programs. We reduce the computation of an quantitative loop invariant to solving constraints over program variables and unknown coefficients. Lagrange interpolation allows us to find constraints with less unknown coefficients. Counterexample-guided refinement furthermore generates linear constraints that pinpoint the desired quantitative invariants. We evaluate our technique by several case studies with polynomial quantitative loop invariants in the experiments.

cs.SE↗

arXiv2014

A Finite Exact Representation of Register Automata Configurations

A register automaton is a finite automaton with finitely many registers ranging from an infinite alphabet. Since the valuations of registers are infinite, there are infinitely many configurations. We describe a technique to classify infinite register automata configurations into finitely many exact representative configurations. Using the finitary representation, we give an algorithm solving the reachability problem for register automata. We moreover define a computation tree logic for register automata and solve its model checking problem.

cs.FL↗