Publications associées à A Formally Verified NAT Stack

Bridging Monte Carlo worlds: a new framework for accelerator simulations applied on shielding and machine protection studies

This thesis delves into the critical study of particle transport in matter, particularly emphasising its implications for machine protection at CERN's accelerator complex and facilities. To conduct studies of this nature, FLUKA and Geant4 stand out within ...

EPFL2024

Secure Interface Design Leveraging Hardware/Software Support

Atri Bhattacharyya

Computer systems rely heavily on abstraction to manage the exponential growth of complexity across hardware and software. Due to practical considerations of compatibility between components of these complex systems across generations, developers have favou ...

EPFL2024

ACTOR: Action-Guided Kernel Fuzzing

Mathias Josef Payer

Fuzzing reliably and efficiently finds bugs in software, including operating system kernels. In general, higher code coverage leads to the discovery of more bugs. This is why most existing kernel fuzzers adopt strategies to generate a series of inputs that ...

Usenix Assoc2023

Scalable Metaprogramming in Scala 3

Nicolas Alexander Stucki

A metaprogrammer should be able to reason about the semantics of the generated code. Multi-stage programming introduced an elegant and powerful solution to this problem. It follows a semantically driven approach to code generation, where semantics are full ...

EPFL2023

Midas: Systematic Kernel TOCTTOU Protection

Atri Bhattacharyya, Uros Tesic, Mathias Josef Payer

Double-fetch bugs are a plague across all major operating system kernels. They occur when data is fetched twice across the user/kernel trust boundary while allowing concurrent modification. Such bugs enable an attacker to illegally access memory, cause den ...

2022

Relaxed Locally Correctable Codes With Nearly-Linear Block Length And Constant Query Complexity

Alessandro Chiesa

Locally correctable codes (LCCs) are error correcting codes C : \Sigmak \rightarrow \Sigman which admit local algorithms that correct any individual symbol of a corrupted codeword via a minuscule number of queries. For systematic codes, this notion is stro ...

SIAM PUBLICATIONS2022

Symmetry in design and decoding of polar-like codes

Kirill Ivanov

The beginning of 21st century provided us with many answers about how to reach the channel capacity. Polarization and spatial coupling are two techniques for achieving the capacity of binary memoryless symmetric channels under low-complexity decoding algor ...

EPFL2022

NrOS: Effective Replication and Sharing in an Operating System

Sanidhya Kashyap, Ankit Bhardwaj

Writing a correct operating system kernel is notoriously hard. Kernel code requires manual memory management and type-unsafe code and must efficiently handle complex, asynchronous events. In addition, increasing CPU core counts further complicate kernel de ...

USENIX ASSOC2021

Polarization-Adjusted Convolutional (PAC) Codes: Sequential Decoding vs List Decoding

Andreas Peter Burg, Mohammad Rowshan

In the Shannon lecture at the 2019 International Symposium on Information Theory (ISIT), Arikan proposed to employ a one-to-one convolutional transform as a pre-coding step before the polar transform. The resulting codes of this concatenation are called po ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2021

Rebooting Virtual Memory with Midgard

Babak Falsafi, Atri Bhattacharyya, Siddharth Gupta, Mathias Josef Payer, Yunho Oh, Abhishek Bhattacharjee

Computer systems designers are building cache hierarchies with higher capacity to capture the ever-increasing working sets of modern workloads. Cache hierarchies with higher capacity improve system performance but shift the performance bottleneck to addres ...

2021

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 code ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2020

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

On the Computational Complexity of Blind Detection of Binary Linear Codes

Alexios Konstantinos Balatsoukas Stimming, Aris Filos Ratsikas

In this work, we study the computational complexity of the Minimum Distance Code Detection problem. In this problem, we are given a set of noisy codeword observations and we wish to find a code in a set of linear codes C of a given dimension k, for which t ...

IEEE2019

Reed-Muller codes polarize

Emmanuel Abbé, Min Ye

Reed-Muller (RM) codes were introduced in 1954 and have long been conjectured to achieve Shannon's capacity on symmetric channels. The activity on this conjecture has recently been revived with the emergence of polar codes. RM codes and polar codes are gen ...

IEEE COMPUTER SOC2019

Permutation-based Decoding of Reed-Muller Codes in Binary Erasure Channel

Rüdiger Urbanke, Kirill Ivanov

In this paper, we consider the problem of decoding Reed-Muller (RM) codes in binary erasure channel. We propose a novel algorithm, which exploits several techniques, such as list recursive (successive cancellation) decoding based on Plotkin decomposition, ...

IEEE2019

Gaussian channel transmission of images and audio files using cryptcoding

Vladimir Ilievski

Random codes based on quasigroups (RCBQ) are cryptcodes, i.e. they are error-correcting codes, which provide information security. Cut-Decoding and 4-Sets-Cut-Decoding algorithms for these codes are defined elsewhere. Also, the performance of these codes f ...

2019

Prefetched Address Translation

Boris Robert Grot, Edouard Bugnion, Dmitrii Ustiugov

With explosive growth in dataset sizes and increasing machine memory capacities, per-application memory footprints are commonly reaching into hundreds of GBs. Such huge datasets pressure the TLB, resulting in frequent misses that must be resolved through a ...

ASSOC COMPUTING MACHINERY2019

A Formally Verified NAT Stack

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardwar ...

ASSOC COMPUTING MACHINERY2018

Design rules for optimizing unipolar coded Brillouin optical time-domain analyzers

Luc Thévenaz, Marcelo Alfonso Soto Hernandez, Simon Adrien Zaslawski, Zhisheng Yang, Zonglei Li

The performance of unipolar unicolor coded Brillouin optical time-domain analysis (BOTDA) is evaluated based on both Simplex and Golay codes. Four major detrimental factors that limit the system performance, including decoded-gain trace distortion, coding ...

2018

High-Dimensional Inference on Dense Graphs with Applications to Coding Theory and Machine Learning

Mohamad Baker Dia

We are living in the era of "Big Data", an era characterized by a voluminous amount of available data. Such amount is mainly due to the continuing advances in the computational capabilities for capturing, storing, transmitting and processing data. However, ...

EPFL2018