Publications related to Computer Science Laboratory has three large edges

Automated Verification of Network Function Binaries

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF binaries, making verification usable by network operators even on proprietary code. To solve the key challenge of bridging the abstraction levels of NF implementations and specifications without special-casing a set of data structures, we observe that data structures used by NFs can be modeled as maps, and introduce a universal type to specify both NFs and their data structures, the "ghost map". In addition, we observe that the interactions between an NF and its environment are sufficient to infer control flow and types, removing the requirement for source code. We implement our technique in Klint, a tool with which we verify, in minutes, that 7 NF binaries satisfy their specifications, without limiting developers' choices of data structures. The specifications are written in Python and use maps to model state. Klint can also verify an entire NF binary stack, all the way down to the NIC driver, using a minimal operating system. Operators can thus verify NF binaries, without source code or debug symbols, without requiring developers to use specific programming languages or data structures, and without trusting any software except Klint.

USENIX Association2022

TEE-based decentralized recommender systems: The raw data sharing redemption

Akash Balasaheb Dhasade, Nevena Dresevic, Anne-Marie Kermarrec, Rafael Pereira Pires

Recommenders are central in many applications today. The most effective recommendation schemes, such as those based on collaborative filtering (CF), exploit similarities between user profiles to make recommendations, but potentially expose private data. Federated learning and decentralized learning systems address this by letting the data stay on user's machines to preserve privacy: each user performs the training on local data and only the model parameters are shared. However, sharing the model parameters across the network may still yield privacy breaches. In this paper, we present REX, the first enclave-based decentralized CF recommender. REX exploits Trusted execution environments (TEE), such as Intel software guard extensions (SGX), that provide shielded environments within the processor to improve convergence while preserving privacy. Firstly, REX enables raw data sharing, which ultimately speeds up convergence and reduces the network load. Secondly, REX fully preserves privacy. We analyze the impact of raw data sharing in both deep neural network (DNN) and matrix factorization (MF) recommenders and showcase the benefits of trusted environments in a full-fledged implementation of REX. Our experimental results demonstrate that through raw data sharing, REX significantly decreases the training time by 18.3x and the network load by 2 orders of magnitude over standard decentralized approaches that share only parameters, while fully protecting privacy by leveraging trustworthy hardware enclaves with very little overhead.

2022

Watermarking-based Defense against Adversarial Attacks on Deep Neural Networks

James Richard Larus, Xiaoting Li, Dinghao Wu, Junjun Zhang

The vulnerability of deep neural networks to adversarial attacks has posed significant threats to real-world applications, especially security-critical ones. Given a well-trained model, slight modifications to the input samples can cause drastic changes in the predictions of the model. Many methods have been proposed to mitigate the issue. However, the majority of these defenses have proven to fail to resist all the adversarial attacks. This is mainly because the knowledge advantage of the attacker can help to either easily customize the information of the target model or create a surrogate model as a substitute to successfully construct the corresponding adversarial examples. In this paper, we propose a new defense mechanism that creates a knowledge gap between attackers and defenders by imposing a designed watermarking system into standard deep neural networks. The embedded watermark is data-independent and non-reproducible to an attacker, which improves randomization and security of the defense model without compromising performance on clean data, and thus yields knowledge disadvantage to prevent an attacker from crafting effective adversarial examples targeting the defensive model. We evaluate the performance of our watermarking defense using a wide range of watermarking algorithms against four state-of-the-art attacks on different datasets, and the experimental results validate its effectiveness.

IEEE2021

Software Support for Non-Volatile Memory (NVM) Programming

David Teksen Aksun

Non-Volatile Memory (NVM) is an emerging type of memory device that provides fast, byte-addressable, and high-capacity durable storage. NVM sits on the memory bus and allows durable data structures designs similar to the in-memory equivalent ones. Expensive serialization/deserialization operations, usually associated with block-based storage, are not necessary. Unfortunately, using NVM is not as simple as placing a data structure in NVM and expecting persistence. As NVM sits on the memory bus, processor caches buffer the cache lines from it that are referenced by load and store instructions. The volatility of the caches and possible power failures at a random point in a program complicate the design and require ways to handle these failures. Prior work focused on implementing crash-consistency mechanisms to correctly recover a program's data after a failure. The goal was to minimize the use of costly cache line write-back and fence instructions, which are necessary for correct durability. Moreover, commercial NVM devices are slower compared to DRAM and affect the design. In addition to performance overheads, correctly implementing crash consistency is hard. The programmers need to carefully reason about cache line write-back instructions and the order of persistent writes. Finding bugs can take from minutes to hours. In this thesis, we use checkpointing as an effective crash-consistency mechanism with low overhead for building durable data structures. We also describe an inter-procedural dataflow analysis for fast detection of NVM programming bugs. We show the practicality of these ideas through three primary contributions and their implementations. Firstly, we present InCLL to address NVM checkpointing. InCLL is a novel technique that uses fine-grained checkpointing and in-cache-line logging to minimize the number of explicit write-back and fence instructions in the fast path of data structure modifications. We evaluate InCLL both on DRAM and Optane devices for the Masstree data structure. Secondly, we present a new checkpointing design, CpNvm, which minimizes NVM write-back instructions on the critical path of the execution. We achieve low overheads for Masstree and Memcached for write-heavy workloads, and almost no overheads for read-only workloads. In addition, we present FlowNvm to find NVM programming bugs. FlowNvm can identify NVM programming pattern violations and anti-patterns at compile-time using inter-procedural dataflow analysis.

EPFL2021

Programming Heterogeneous CPU-GPU Systems by High-Level Dataflow Synthesis

Endri Bezati, Aurélien François Gilbert Bloch, Marco Mattavelli

Heterogeneous processing platforms combining in various architectures CPUs, GPUs, and programmable logic, are continuously evolving providing at each generation higher theoretical levels of computing performance. However, the challenge of how efficiently specify and explore the design space of applications executing on the different components of heterogeneous platforms remains an open problem and is the subject of many research efforts. The paper describes a dataflow based approach for the synthesis of applications to be executed on mixed CPU and GPU architectures. The new high-level approach consists of partitioning the application dataflow program written in RVC-CAL into CPU and GPU components, then on generating by automatic synthesis the C++ and CUDA programs that together implement the application executable. The design approach provides portability of applications on CPUs, GPUs, and mixed CPU/GPU architectures as well as the possibility of exploring the design space of all partitioning options without the need of rewriting the application code. The paper describes the essential methodology features at the base of the synthesis of CPU/GPU code and reports some example design cases validating the correctness of the approach.

IEEE2020

, , , ,

Programming languages and systems have failed to address the security implications of the increasingly frequent use of public libraries to construct modern software. Most languages provide tools and online repositories to publish, import, and use libraries; however, this double-edged sword can incorporate a large quantity of unknown, unchecked, and unverified code into an application. The risk is real, as demonstrated by malevolent actors who have repeatedly inserted malware into popular open-source libraries. This paper proposes a solution: enclosures, a new programming language construct for library isolation that provides a developer with fine-grain control over the resources that a library can access, even for libraries with complex inter-library dependencies. The programming abstraction is language-independent and could be added to most languages. These languages would then be able to take advantage of hardware isolation mechanisms that are effective across language boundaries. The enclosure policies are enforced at run time by LitterBox, a language-independent framework that uses hardware mechanisms to provide uniform and robust isolation guarantees, even for libraries written in unsafe languages. LitterBox currently supports both Intel VT-x (with general-purpose extended page tables) and the emerging Intel Memory Protection Keys (MPK). We describe an enclosure implementation for the Go and Python languages. Our evaluation demonstrates that the Go implementation can protect sensitive data in real-world applications constructed using complex untrusted libraries with deep dependencies. It requires minimal code refactoring and incurs acceptable performance overhead. The Python implementation demonstrates LitterBox’s ability to support dynamic languages.

2021

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that performance and simplicity can coexist, at the cost of some flexibility, with a new NIC driver model tailored to network functions. The key idea behind our model is that the driver can efficiently reuse packet buffers because buffers follow a single logical path. We implement a driver for the Intel 82599 network card in 550 lines of code. By merely replacing the state-of-theart driver with our driver, formal verification of the entire software stack completes in 7x less time, while the verified functions’ throughput improves by 160%. Our driver also beats, on realistic workloads, the throughput of drivers that cannot yet be formally verified, thanks to its low variability and resource use. Our code is available at github.com/dslab-epfl/tinynf.

2021

OneFile: A Wait-free Persistent Transactional Memory

Nachshon Cohen, Pascal Felber

A persistent transactional memory (PTM) library provides an easy-to-use interface to programmers for using byte-addressable non-volatile memory (NVM). Previously proposed PTMs have, so far, been blocking. We present OneFile, the first wait-free PTM with integrated wait-free memory reclamation. We have designed and implemented two variants of the OneFile, one with lock-free progress and the other with bounded wait-free progress. We additionally present software transactional memory (STM) implementations of the lock-free and wait-free algorithms targeting volatile memory. Each of our PTMs and STMs is implemented as a single C++ file with 1,000 lines of code, making them versatile to use. Equipped with these PTMs and STMs, non-expert developers can design and implement their own lock-free and wait-free data structures on NVM, thus making lock-free programming accessible to common software developers.

IEEE COMPUTER SOC2019

System and method for decoding reed-muller codes

Emmanuel Abbé, Min Ye

Various embodiments are directed to Reed-Muller decoding systems and methods based on recursive projections and aggregations of cosets decoding, exploiting the self-similarity of RM codes, and extended with list-decoding procedures and with outer-code concatenations

2020

Recursive Projection-Aggregation Decoding of Reed-Muller Codes

Emmanuel Abbé, Min Ye

We propose a new class of efficient decoding algorithms for Reed-Muller (RM) codes over binary-input memoryless channels. The algorithms are based on projecting the code on its cosets, recursively decoding the projected codes (which are lower-order RM codes), and aggregating the reconstructions (e.g., using majority votes). We further provide extensions of the algorithms using list-decoding. We run our algorithm for AWGN channels and Binary Symmetric Channels at the short code length (

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2020