Search for: All records

Membership inference attacks (MIAs) are currently considered one of the main privacy attack strategies, and their defense mechanisms have also been extensively explored. However, there is still a gap between the existing defense approaches and ideal models in both performance and deployment costs. In particular, we observed that the privacy vulnerability of the model is closely correlated with the gap between the model's data-memorizing ability and generalization ability. To address it, we propose a new architecture-agnostic training paradigm called Center-based Relaxed Learning (CRL), which is adaptive to any classification model and provides privacy preservation by sacrificing a minimal or no loss of model generalizability. We emphasize that CRL can better maintain the model's consistency between member and non-member data. Through extensive experiments on common classification datasets, we empirically show that this approach exhibits comparable performance without requiring additional model capacity or data costs. 

Collecting evidence of data that software systems produce and consume can provide critical information for reconstructing erratic behavior, tracing the origin of faults, and thus holding the responsible party accountable for particular consequences. However, when data propagates across trust boundaries with conflicting interests, they can be tempted to make evidence unprovable in order to avoid potential liability. Hence, we present a data propagation protocol that makes such attempts either detectable or ineffective by having data transfers witnessed by other network participants that collectively act as the prover for the data propagation process. The protocol builds an unstructured peer-to-peer overlay and is designed to disincentivize collusion among a malicious coalition of nodes by enforcing network participants to constantly exchange their partial views on the network in a random yet verifiable manner. A data producer or consumer who does not faithfully follow the protocol ends up having fewer witnesses from their side, making the network resistant to collusion with high probability. We derive the conditions under which this property holds and demonstrate the practicality and cost of our approach through the implementation of a distributed application built on top of the proposed protocol. 

Real-time systems power safety-critical applications that require strong isolation among each other. Such isolation needs to be enforced at two orthogonal levels. On the micro-architectural level, this mainly involves avoiding interference through micro-architectural states, such as cache lines. On the algorithmic level, this is usually achieved by adopting real-time partitions to reserve resources for each application. Implementations of such systems are often complex and require formal verification to guarantee proper isolation. In this paper, we focus on algorithmic isolation, which is mainly related to scheduling-induced interferences. We address earliest-deadline-first (EDF) partitions to achieve compositionality and utilization, while imposing constraints on tasks' periods and enforcing budgets on these periodic partitions to ensure isolation between each other. The formal verification of such a real-time OS kernel is challenging due to the inherent complexity of the dynamic priority assignment on the partition level. We tackle this problem by adopting a dynamically constructed abstraction to lift the reasoning of a concrete scheduler into an abstract domain. Using this framework, we verify a real-time operating system kernel with budget-enforcing EDF partitions and prove that it indeed ensures isolation between partitions. All the proofs are mechanized in Coq.