Publications related to A Simpler and Faster NIC Driver Model for Network Functions

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Task-driven neural network models predict neural dynamics of proprioception: Experimental data, activations and predictions of neural network models

Axel Bisi, Alberto Silvio Chiappa, Alexander Mathis, Alessandro Marin Vargas

Here we provide the neural data, activation and predictions for the best models and result dataframes of our article "Task-driven neural network models predict neural dynamics of proprioception". It contains the behavioral and neural experimental data (cu ...

EPFL Infoscience2024

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Performance Interfaces for Network Functions

George Candea, Aikaterini Argyraki, Rishabh Ramesh Iyer

Modern programmers routinely use third-party code, and infrastructure operators deploy software they did not write. This would not be possible without semantic interfaces---documentation, header files, specifications---that succinctly describe what that th ...

USENIX Association2022

Attacks on some post-quantum cryptographic protocols: The case of the Legendre PRF and SIKE

Novak Kaluderovic

Post-quantum cryptography is a branch of cryptography which deals with cryptographic algorithms whose hardness assumptions are not based on problems known to be solvable by a quantum computer, such as the RSA problem, factoring or discrete logarithms. This ...

EPFL2022

Direct Model-checking of SysML Models

Alessandro Tempia Calvino

Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a ne ...

SCITEPRESS2021

Full key recovery side-channel attack against ephemeral SIKE on the Cortex-M4

Aymeric Genet, Natacha Yolande Emmanuel Marie Linard de Guertechin, Novak Kaluderovic

This paper describes the first practical single-trace side-channel power analysis of SIKE. While SIKE is a post-quantum key exchange, the scheme still relies on a secret elliptic curve scalar multiplication which involves a loop of a double-and-add procedu ...

2021

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

Optimization and Generalization of Shallow Neural Networks with Quadratic Activation Functions

Lenka Zdeborová

p>We study the dynamics of optimization and the generalization properties of one-hidden layer neural networks with quadratic activation function in the overparametrized regime where the layer width m is larger than the input dimension d. We conside ...

Curran Associates, Inc.2020

Disentangling feature and lazy training in deep neural networks

Mario Geiger, Arthur Ulysse Jacot-Guillarmod, Matthieu Wyart, Stefano Spigler, Arthur Jacot

Two distinct limits for deep learning have been derived as the network width h -> infinity, depending on how the weights of the last layer scale with h. In the neural tangent Kernel (NTK) limit, the dynamics becomes linear in the weights and is described b ...

IOP PUBLISHING LTD2020

Verifying Software Network Functions with No Verification Expertise

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Matteo Rizzo

We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write ...

ACM2019

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

How single neuron properties shape chaotic dynamics and signal transmission in random neural networks

Wulfram Gerstner, Tilo Schwalger, Samuel Pavio Muscinelli

While most models of randomly connected neural networks assume single-neuron models with simple dynamics, neurons in the brain exhibit complex intrinsic dynamics over multiple timescales. We analyze how the dynamical properties of single neurons and recurr ...

2019

Automated Synthesis of Adversarial Workloads for Network Functions

Aikaterini Argyraki, Jonas Fietz, Arseniy Zaostrovnykh, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa

Software network functions promise to simplify the deployment of network services and reduce network operation cost. However, they face the challenge of unpredictable performance. Given this performance variability, it is imperative that during deployment, ...

ACM2018

Implications of Position in Cryptography

Handan Kilinç Alper

In our daily lives, people or devices frequently need to learn their location for many reasons as some services depend on the absolute location or the proximity. The outcomes of positioning systems can have critical effects e.g., on military, emergency. Th ...

EPFL2018

Neural Tanget Kernel: Convergence and Generalization in Neural Networks

Clément Hongler, Arthur Ulysse Jacot-Guillarmod, Franck Raymond Gabriel

At initialization, artificial neural networks (ANNs) are equivalent to Gaussian processes in the infinite-width limit [12, 9], thus connecting them to kernel methods. We prove that the evolution of an ANN during training can also be described by a kernel: ...

NEURAL INFORMATION PROCESSING SYSTEMS (NIPS)2018

A Formally Verified NAT

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Towards Proving Optimistic Multicore Schedulers

Willy Zwaenepoel, Baptiste Joseph Eustache Lepers

Operating systems have been shown to waste machine resources by leaving cores idle while work is ready to be scheduled. This results in suboptimal performance for user applications, and wasted power. Recent progress in formal verification methods have led ...

2017

Simplifying Development and Management of Software-Defined Networks

Peter Peresini

Computer networks are an important part of our life. Yet, they are traditionally hard to manage and operate. The recent shift to Software-Defined Networking (SDN) is promised to change the way in which the networks are run by their operators. However, SDN ...

EPFL2016

Approximate BDD Optimization with Prioritized epsilon-Preferred Evolutionary Algorithm

Mathias Soeken

Approximate computing has gained high attention in various applications that can benefit from a reduction in costs by lowering the accuracy. In this paper we present an optimization approach for functional approximation of Binary Decision Diagrams (BDDs) w ...

Assoc Computing Machinery2016