The Ei/Ψ seminar at Technische Universiteit Eindhoven is currently organized by
Arpan A Ray and Subhasree Patro.
The seminar is aimed at the crypto and security groups at TU/e.
If you are interested in presenting your research, please let us know by emailing
a.a.ray (at) tue.nl and/or s.patro (at) tue.nl.
We especially encourage presentations of work in progress or open problems
to stimulate future joint work.
The talks should be 45 minutes including questions.
Credits: This page was previously maintained by Michelle Campobasso (till 2023), and before that by Lorenz Panny and Daan Leermakers, who have been organising the seminars until February 2021.
-
Time & place:
8 March 2022 at 13:00 (online)
Speaker:
Matthias Meijers (TU/e)
Title:
Formal Verification of Saber
Abstract:
This work concerns the formal verification of Saber's public-key encryption scheme in EasyCrypt.
Here, "Saber" is one of the finalists in the currently ongoing competition held by NIST with the purpose of standardizing post-quantum cryptography; "EasyCrypt" is a tool specifically designed for the formal verification of cryptographic constructions.
The talk will go over the relevant context and motivation for the work, the most important/interesting aspects of the formal verification process (for Saber in EasyCrypt), the obtained results, and some opportunities for potential future work.
-
Time & place:
8 February 2022 at 13:00 (online)
Speaker:
Boris Škorić (TU/e)
Title:
Can't touch this
Abstract:
Storing data on an external server with information-theoretic security, while using a key shorter than the data itself, is impossible. As an alternative, we propose a scheme that achieves information-theoretically secure evidence of accessing: The server is able to obtain information about the stored data, but not while staying undetected. Moreover, the client only needs to remember a key whose length is much shorter than the data. We provide a security proof for our scheme, based on an entropic uncertainty relation, similar to QKD proofs. Our scheme works if Alice is able to (reversibly) randomise the message to almost-uniformity with only a short key. By constructing an explicit attack we show that the desired security properties cannot be achieved without this randomisability.
Link to paper:
arXiv
-
Time & place:
15 September 2021 at 13:00 (online)
Speaker:
Arne Aarts (TU/e)
Title:
Leveraging Partial Model Extractions using Uncertainty Quantification
Abstract:
Companies have started to offer paid access to machine learning models as a service (MLaaS). The creation of said models requires the gathering curating and labeling of large amounts of data, which is a costly and time-consuming process. Providing black box access to the model unfortunately leaves one open to cloning attacks. With sufficiently many queries spend to the service it is possible to create a surrogate dataset and extract a clone of the underlying ML model, subverting the business model. We present a new cloning scheme that uses uncertainty quantification (UQ) to get arbitrarily close to the accuracy of the service for any amount of queries spend at the cost of needing to delegate a fraction of inputs to the service. In this two-step scheme the adversary first creates a "partial" clone using a conventional cloning attack with a small number of queries. Next, during inference the adversary uses UQ to decide whether the output of the partial clone is likely in line with that of the service. If not, it will delegate the input to the service and substitute its own output with that of the service. This way an adversary can set up their own competing service leeching from the original. Using this scheme, the overall costs made in terms of queries can be minimized given an expected number of sales such that the adversary can turn a profit. Compared to previous attacks the new scheme allows for significant lower initial costs, ensures an accuracy arbitrarily close to that of the targeted service, and can result in overall lower costs.
-
Time & place:
27 May 2021 at 13:00 (online)
Speaker:
Eleftheria Makri (KU Leuven)
Title:
The return of Eratosthenes: Secure Generation of RSA Moduli using Distributed Sieving
Abstract:
Secure multiparty generation of an RSA biprime is a challenging task, which increasingly receives attention, due to the numerous privacy-preserving applications that require it. In this work, we construct a new protocol for the RSA biprime generation task, secure against a malicious adversary, who can corrupt any subset of protocol participants. Our protocol is designed for generic MPC, making it both platform-independent and allowing for weaker security models to be assumed (e.g., honest majority), should the application scenario require it. By carefully ``postponing" the check of possible inconsistencies in the shares provided by malicious adversaries, we achieve noteworthy efficiency improvements. Concretely, we are able to produce additive sharings of the prime candidates, from multiplicative sharings via a semi-honest multiplication, without degrading the overall (active) security of our protocol. This is the core of our sieving technique, increasing the probability of our protocol sampling a biprime. Similarly, we perform the first biprimality test, requiring several repetitions, without checking input share consistency, and perform the more costly consistency check only in case of success of the Jacobi symbol based biprimality test. Moreover, we propose a protocol to convert an additive sharing over a ring, into an additive sharing over the integers. Besides being a necessary sub-protocol for the RSA biprime generation, this conversion protocol is of independent interest. The cost analysis of our protocol demonstrated that our approach improves the current state-of-the-art (Chen et al. -- Crypto 2020), in terms of communication efficiency. Concretely, for the two-party case with malicious security, and primes of 2048 bits, our protocol improves communication by a factor of ~37.
Video link:
YouTube
-
Time & place:
6 April 2021 at 13:00 (online)
Speaker:
Raluca Posteuca (KU Leuven)
Title:
How to backdoor a cipher
Abstract:
Newly designed block ciphers are required to show resistance against known attacks, e.g., linear and differential cryptanalysis. Two widely used methods to do this are to employ an automated search tool (e.g., MILP, SAT/SMT, etc.) and/or provide a wide-trail argument. In both cases, the core of the argument consists of bounding the transition probability of the statistical property over an isolated non-linear operation, then multiply it by the number of such operations (e.g., number of active S-boxes).
In this talk we show that in the case of linear cryptanalysis such strategies can sometimes lead to a gap between the claimed security and the actual one, and that this gap can be exploited by a malicious designer. We introduce Rood, a block cipher with a carefully crafted backdoor. By using the means of the wide-trail strategy, we argue the resistance of the cipher against linear and differential cryptanalysis. However, the cipher has a key-dependent iterative linear approximation over 12 rounds, holding with probability 1. This property is based on the linear hull effect although any linear trail underlying the linear hull has probability smaller than 1.
-
Time & place:
13 October 2020 at 10:00 (online)
Speaker:
Michele Campobasso (TU/e)
Title:
Impersonation-as-a-Service: Characterizing the Emerging Criminal Infrastructure for User Impersonation at Scale
Abstract:
In this paper we provide evidence of an emerging criminal infrastructure enabling impersonation attacks at scale. Impersonation-as-a-Service (ImpaaS) allows attackers to systematically collect and enforce user profiles (consisting of user credentials, cookies, device and behavioural fingerprints, and other metadata) to circumvent risk-based authentication system and effectively bypass multi-factor authentication mechanisms. We present the ImpaaS model and evaluate its implementation by analysing the operation of a large, invite-only, Russian ImpaaS platform providing user profiles for more than 260'000 Internet users worldwide. Our findings suggest that the ImpaaS model is growing, and provides the mechanisms needed to systematically evade authentication controls across multiple platforms, while providing attackers with a reliable, up-to-date, and semi-automated environment enabling target selection and user impersonation against Internet users as scale.
-
Time & place:
16 December 2019 at 12:30 (MF 3)
Speaker:
Mina Sheikhalishahi (TU/e)
Title:
Privacy-preserving Multi-party Access Control
Abstract:
Multi-party access control has been proposed to enable collaborative decision making for the protection of co-owned resources. In particular, multi-party access control aims to reconcile conflicts arising from the evaluation of policies authored by different stakeholders for jointly-managed resources, thus determining whether access to those resources should be granted or not. While providing effective solutions for the protection of co-owned resources, existing approaches do not address the protection of policies themselves, whose disclosure can leak sensitive information about, e.g., the relationships of co-owners with other parties. In this paper, we propose a privacy-preserving multi-party access control mechanism, which preserves the confidentiality of user policies. In particular, we propose secure computation protocols for the evaluation of multi-party policies, based on two privacy-preserving techniques, namely homomorphic encryption and secure function evaluation. An experimental evaluation of our approach shows its practical feasibility in terms of both computation and communication costs.
-
Time & place:
2 December 2019 at 12:30 (MF14)
Speaker:
Pavlo Burda (TU/e)
Title:
Phishing experiments with humans, or the effectiveness of tailored phishing techniques
Abstract:
Organizations worldwide are observing the appearance of more and more sophisticated attacks specifically targeting their employees and customers alike. These attacks exploit tailored information on the victim or organization to increase their credibility. To date, no study has evaluated the role of 'traditional' phishing cognitive effects in these advanced settings. In this paper, we run a phishing controlled experiment targeting 747 subjects employed in two organizations (a university and a large, international consultancy company) to evaluate the interaction between phishing persuasion techniques and success rate in a highly-tailored setting. For this purpose, we borrow from the user notification literature to devise enhanced attack delivery techniques, and evaluate how such techniques affect the success rate of our phishing campaigns. We find that the effect of 'traditional' attack techniques is widely mitigated in highly-tailored phishing settings, suggesting that current user training and detection techniques may be off-target for more sophisticated attacks.
However, we find that the means by which the attack is delivered to the victim matter, and can greatly (up to three times) boost the effect of the attack in its base form.
-
Time & place:
31 October 2019 at 12:30 (MF2)
Speaker:
Sowmya Ravidas (TU/e)
Title:
On Attribute Retrieval in ABAC
Abstract:
Despite the growing interest in Attribute-Based Access Control (ABAC) and the large amount of research devoted to the specification and evaluation of ABAC policies, to date only little work has addressed the issue of attribute management and retrieval. In modern systems, the attributes needed for policy evaluation are often retrieved from external sources (e.g., sensors, access points). This poses concerns on the correctness of policy evaluation as the policy decision point can be provided with incorrect attribute values, which can potentially yield incorrect decisions. In this talk, we present our investigation on the problem of selecting mechanisms for attribute retrieval and its relation with the accuracy of policy evaluation. We first introduce the notion of policy evaluation under error rate and use this notion to compute the evaluation accuracy of a policy. We formulate the Attribute Retrieval Mechanism Selection Problem (ARMSP) in terms of evaluation accuracy and show that ARMSP is exponential in the number of attribute values. To overcome this computation limitation, we investigate approaches to estimate the evaluation accuracy of a policy while maintaining the computation feasible.
-
Time & place:
21 October 2019 at 12:30 (MF15)
Speaker:
Guillaume Dupont (TU/e)
Title:
Evaluation Framework for Network Intrusion Detection Systems for In-Vehicle CAN
Abstract:
Abstract Modern vehicles are complex safety critical cyber physical systems, that are connected to the outside world, with all security implications it brings. Different network intrusion detection systems (NIDSs) proposed for the CAN bus, the predominant type of in-vehicle network, to improve security are hard to compare due to disparate evaluation methods adopted.
In this paper we provide the means to compare CAN NIDSs on equal footing and evaluate the ones detailed in the literature. Based on this we observe some limitation of existing approaches and why in the CAN setting it is intrinsically difficult to distinguish benign from malicious payload. We argue that "meaning-aware" detection (a concept we define) which is challenging (but perhaps not impossible) to create for this setting.
-
Time & place:
7 October 2019 at 12:30 (MF14)
Speaker:
Jana Sotáková (CWI/UvA)
Title:
Adventures in Supersingularland
Abstract:
The problem of path finding in supersingular isogeny graphs has recently been proposed as a hard problem underlying the post-quantum key exchange scheme SIKE. So far, both quantum and classical attacks have exponential time complexity. However, for a small subset of the vertices, the Spine, path-finding is much easier. For cryptanalysis, the Spine is typically assumed to be randomly distributed through the graph. We will look at many examples of isogeny graphs to show how the Spine sits inside the supersingular isogeny graph.
This is joint work with Sarah Arpin, Catalina Camacho-Navarro, Kristin Lauter, Joelle Lim, Kristina Nelson and Travis Scholl.
-
Time & place:
26 August 2019 at 11:00 (Atlas 4.224)
Speaker:
Guillaume Dupont (TU/e)
Title:
A Survey of Network Intrusion Detection Systems for Controller Area Network
Abstract:
Modern vehicles are complex safety critical cyber physical systems, that are connected to the outside world, with all security implications that brings. To enhance vehicle security several network intrusion detection systems (NIDS) have been proposed for the CAN bus, the predominant type of in-vehicle network.
The in-vehicle CAN bus, however, is a challenging place to do intrusion detection as
messages provide very little information; interpreting them requires specific knowledge about the implementation that is not readily available. In this paper we collect how existing solutions address this challenge by providing an organized inventory of frame based CAN NIDS proposed in literature, categorizing them based on what information they extract from the network and how they build their model.
-
Time & place:
8 July 2019 at 12:30 (MF14)
Speaker:
Sofía Celi
Title:
OTRv4, the newest version of the Off-The-Record protocol
Abstract:
OTRv4 is the newest version of the Off-The-Record protocol.
As a Privacy Enhancing Technology, it is a protocol where the newest
academic research intertwines with real-world implementations. This new
version asks us to revisit definitions around deniability
(participation, message, online and offline), forward and
post-compromise secrecy, and how important they are to the world. In
this talk, we will examine the key security properties that secure
messaging protocols and applications should have. We will explore how
these properties are achieved in OTRv4, in particular, and why they are
needed in today’s world.
-
Time & place:
17 June 2019 at 12:30 (MF15)
Speaker:
Chloe Martindale (TU/e)
Title:
Are pairings really dead?
Abstract:
We will discuss pairings of elliptic curves: a cryptographic primitive used in identity-based encryption and a fundamental building block of privacy protocols. Pairings suffered a blow in 2016 — an improved attack slowing down the favourite constructions in the literature — leading some cryptographers to assume that pairings are dead.
We will first give some background on pairings, and then discuss some recent works (not only mine) presenting constructions of pairings for which the lastest attack is ineffective.
This talk will refer to joint work with both Chitchanok Chuengsatiansup and Georgios Fotiadis.
-
Time & place:
27 May 2019 at 12:30 (MF14)
Speaker:
Frank van den Bosch-Blom (TU/e)
Title:
Efficient Secure Ridge Regression from Randomized Gaussian Elimination
Abstract:
We present a practical protocol for secure ridge regression. We develop the necessary secure linear algebra tools, using only basic arithmetic over prime Fields. In particular, we show how to solve linear systems of equations and compute matrix inverses efficiently, using appropriate secure random self-reductions of these problems. The distinguishing feature of our approach is that the use of secure fixed-point arithmetic is avoided entirely, while circumventing the need for rational reconstruction at any stage as well. The effectiveness of our protocol is demonstrated by implementation in a standard setting for information-theoretically secure multiparty computation, tolerating a dishonest minority of passively corrupt parties. Using the MPyC framework, which is based on threshold secret sharing over finite fields, we show how to handle large datasets efficiently, achieving root-mean-square errors arbitrarily close to those of plaintext Scikit-learn. Moreover, we do not assume that any (part) of the datasets is held privately by any of the parties, which makes our protocol much more versatile than previous solutions which utilize assumptions on private held data. Our experiments show that our solution outperforms existing solutions for datasets commonly used for secure ridge regression benchmarking, reaching new heights running efficiently on larger real-world datasets than previous works.
-
Time & place:
13 May 2019 at 12:30 (MF14)
Speaker:
Milan Lopuhaä-Zwakenberg (TU/e)
Title:
Measuring privacy and utility of local privacy protocols
Abstract:
In a setting where an aggregator is interested in users' private data, but the users do not trust the aggregator, an often used solution is to have the users to mask their private data under random noise. That way the aggregator cannot be certain about any individual's private data, but as the random noise averages out they still obtain information about the user population as a whole. The aggregator and the users have competing requirements for the random noise protocol: the aggregator wants reliable information about population statistics (Utility) while the users want to protect their private data (Privacy). In this talk, we will look at commonly used definitions of Privacy and Security for random protocols, their shortcomings, and how new definitions based on information theory give us a better understanding of the functioning of such random protocols.
-
Time & place:
29 April 2019 at 12:30 (MF14)
Speaker:
Lorenz Panny (TU/e)
Title:
Diffie-Hellman reductions
Abstract:
Starting from related classical observations, I will present a recent
result concerning the security of a post-quantum Diffie-Hellman-style
key-exchange protocol in comparison to the corresponding key-recovery
problem.
For those scared of these words: I will explain what they mean, and
I will try to assume no more than some elementary group theory.
While these results have no direct practical application, they form a
beautiful and accessible example of cryptographic hardness reductions.
-
Time & place:
3 April 2019 at 12:30 (MF14)
Speaker:
Gustavo Banegas (TU/e)
Title:
Anything for finding roots
Abstract:
Several code-based schemes use a polynomial called "Error locator
polynomial" (ELP) where the roots of this polynomial is the error
positions that one wants to correct for recovering a noisy codeword that
is "m+e". We are interested in the timing of the operations for
evaluate the roots and the leaks that the current methods provide to us
for gathering information and later on recover the message. Also, we are
interested in how is it possible to fix this problem, what is the impact
of a constant-time implementation of it? Is it possible to do it in
constant-time?
-
Time & place:
11 March 2019 at 12:45 (MF07)
Speaker:
Filip Davidovich
Title:
Security pentesting of the SEC laboratories
Abstract:
This report presents the findings of an external and internal security assessment of Technical University of Eindhoven's Malware Laboratory (B-LAB) and Security Operations Center (SOC) infrastructures, conducted in the period between 1st of September 2018 to 1st of February 2019.
The security assessment was comprised of two critical parts, where the penetration tester impersonated both an external and an internal attacker. In the effort to assess the general security posture of these infrastructures, the penetration tester has conducted general intelligence gathering, comprehensive network scanning and enumeration, vulnerability assessment and confirmation by means of penetration, as well as pivoting within the infrastructure.
The purpose of this engagement was to assess the effectiveness of security measures put in place by Technical University of Eindhoven, further the client, in order to secure confidentiality and integrity of infrastructure's resources, as well as availability of specific systems.
-
Time & place:
11 March 2019 at 12:00 (MF07)
Speaker:
Manos Doulgerakis
Title:
Voronoi cells and the closest vector problem
Abstract:
In my talk I will first try to give a brief introduction to lattices and mention two main problems we want to solve concerning lattices, the shortest vector problem (SVP) and the closest vector problem (CVP). I will then expand on Voronoi cells and how we can use them to solve the closest vector problem. I will mention what is the Voronoi cell of a lattice, how we can find it and how we can use it in order to solve CVP.
Finally I will mention some recent results on the topic.
-
Time & place:
25 February 2019 at 12:30 (MF15)
Speaker:
Jacob Appelbaum (TU/e)
Title:
Crypto plumbing: replay attacks and sequence numbers
Abstract:
Network protocols have different strategies and threat models for
dealing with surveillance, censorship, and with other active tampering.
Many of the strategies rest on pre-masssurveillance assumptions that do
not hold with the adversaries that we know to be relevant.
This talk focuses on a simple concept: sequence numbers and its
relation to replay attacks. Preventing replay attacks is usually
hand-waved away as a local issue or is ambiguously specified in a way
that leaves protocols open to information leakage.
We will explore some of the different strategies while comparing and
contrasting across myriad of contemporary internet protocols.
-
Time & place:
11 February 2019 at 12:30 (MF13)
Speaker:
Thijs Laarhoven (TU/e)
Title:
Lattice-based cryptanalysis
-
Time & place:
7 January 2019 at 12:45 (MF13)
Speaker:
Bram Cappers
Title:
Interactive Visualization of Event Logs for Cybersecurity
Abstract:
Many domains nowadays try to gain insight in complex phenomena by logging their behavior. Telecom companies for instance analyze their communication networks for the presence of fraud, hospitals analyze patient treatments to discover bottlenecks in the process, and companies study their work flows to improve customer satisfaction. The common ground here is that domains are interested in the analysis of (anomalous) behavior in their system by recording events. The definition of "anomalous" behavior unfortunately is often ill-defined. In addition, the number of events and data attributes in real-world data is typically in the order of thousands and more.
In this presentation we will discuss the role of data visualization for the detection and explanation of anomalous system behavior. We will show the application of visualization techniques in the security domain, where we focus on the protection of critical infrastructures against complex virus attacks (a.k.a. Advanced Persistent Threats). The presented techniques however are general enough to be used in other domains.
-
Time & place:
10 December 2018 at 12:45 (MF15)
Speaker:
Laura Genga (TU/e)
Title:
Discovering Anomalous Frequent Patterns From Event Logs
Abstract:
Organizations usually employ security policies to prevent data breaches and to guarantee the smooth execution of their processes. Traditional security mechanisms adopt a preventive approach, enforcing users to adhere to the prescribed policies. These systems are however too inflexible to be used in flexible processes where users often have to deal with unforeseen situations or emergencies (e.g., Health Care). In this contexts, it is crucial for organizations to assess the compliance of their systems to security policies to detect and react to security infringements. In this talk, I will give a short introduction on compliance checking techniques, discussing how they can be used to mitigate security risks for organization processes. In the end, I'll discuss some recent work we have done to infer patterns of anomalous behaviors from event logs.
-
Time & place:
26 November 2018 at 12:45 (MF15)
Speaker:
Davide Fauri (TU/e)
Title:
From Descriptive Data to Actionable Alerts in Network Intrusion Detection Systems
Abstract:
Many large-scale systems are not monolythic, but made of many subsystems that exchange messages over a network. To detect when something goes wrong, Network Intrusion Detection Systems (NIDS) usually monitor these messages, infer the state of the monitored system, and eventually raise alerts to the security operators.
In this talk, I will give an overview on NIDS, and show two examples taken from my previous research: one of an Industrial Control System and one of a Building Automation System.
I will use these examples to explain my view on how the design of a NIDS cannot happen "in a void"; instead, it is influenced by the information that can be extracted from the data sources, and by the information that needs to be conveyed by the alerts.
I will conclude presenting a couple of future research directions that I believe can improve the design of NIDS.
-
Time & place:
12 November 2018 at 12:45 (MF14)
Speaker:
Francisco Revson F. Pereira
Title:
Quantum Error-Correcting Codes: From the Basics to the Research Trends
Abstract:
Quantum error-correcting codes are an essential tool for the practical implementation of quantum computer and quantum communication. In 1996, Robert Calderbank, Peter Shor, and Andrew Steane invented a method to create quantum codes from classical codes, known as the CSS construction. This construction was generalized by Daniel Gottesman with the stabilizer formalism. In this talk, I will give a short introduction of quantum codes, from the definition of errors to the idea of stabilizer formalism. In the end, some current research interests will be shown, ending with some open problems.
-
Time & place:
29 October 2018 at 12:45 (MF14)
Speaker:
Alessandro Amadori (TU/e)
Title:
DFA on AES with Byte External Encodings
Abstract:
Several White-Box implementations of cryptographic algorithms suffer from side-channel inspired attacks like DFA or DCA. The strength of these attacks is that they can be applied automatically and require minimal reverse engineering effort. In order to mount these attacks, an adversary needs access to the input (DCA) or output (DCA or DFA) of the white-box implementation. Because of this, encoding the input and output of the white-box implementation via external encodings is considered an effective countermeasure against these types of attacks. We want to disprove this belief by presenting an efficient attack that, as DFA and DCA, can be applied in a fully automated way, but at the same time is able to cope with byte external encodings.
-
Time & place:
15 October 2018 at 12:45 (MF14)
Speaker:
Milan Lopuhaä-Zwakenberg (TU/e)
Title:
Counting points on algebraic stacks
Abstract:
A general problem in mathematics is the following: 'Given a set of axioms, how many objects exist that satisfy those axioms?' In this talk, we look at some categories of mathematical objects, e.g. elliptic curves and their torsion groups, and we show how the language of algebraic stacks (and algebraic geometry in general) can help us count these objects.
-
Time & place:
1 October 2018 at 12:45 (MF03)
Speaker:
Stefan Thaler (TU/e)
Title:
Deep Learning in Information Security
Abstract:
Machine learning has a long tradition of helping to solve complex information security problems that are difficult to solve manually. Deep Learning(DL) is a sub-field of machine learning, where models are composed of multiple layers of abstraction. In the past few years, there has been an enormous hype about DL, which has also spilled over to information security.
In this talk, I want to shed some light on the hype and explore what is behind it (the talk will feature a Gartner hype cycle). First, I will sketch the core principles of DL, its place in the AI landscape and outline some of the compelling properties of DL algorithms.
Then, I will give an overview of DL research in information security, which consists of two parts: DL applied to information security problems and security properties of DL algorithms.
Finally, I want to highlight some misuses of DL algorithms in information security and want to outline some potential research directions.
-
Time & place:
4 September 2018 at 11:00 (MF14)
Speaker:
Niek J. Bouman (TU/e)
Title:
Verified Multi-Precision Arithmetic for Cryptology in C++, at Run-Time and at Compile-Time (slides)
Abstract:
Multi-precision arithmetic is arithmetic with operands whose size exceeds the machine word-size, on today's computers typically 64-bits.
In this talk, I will talk about the design of a library for multi-precision integer arithmetic for operands in the order of 100–500 bits. Many cryptographic schemes and applications, like elliptic-curve encryption schemes and secure multiparty computation frameworks require multi-precision arithmetic with integers whose bit-lengths lie in that range.
The library is written in "optimizing-compiler-friendly" C++, with an emphasis on the use of fixed-size arrays and particular function-argument-passing styles (including the avoidance of naked pointers) to allow the limbs to be allocated on the stack or even in registers. Depending on the particular functionality, we get close to, or significantly beat the performance of existing libraries for multiprecision arithmetic that employ hand-optimized assembly code.
Beyond the favorable runtime performance, our library is, to the best of the author's knowledge, the first library that offers big-integer computations during compile-time. For example, when implementing finite-field arithmetic with a fixed modulus, this feature enables the automatic precomputation (at compile time) of the special modulus-dependent constants required for Barrett and Montgomery reduction. Another application is to parse (at compile-time) a base-10-encoded big-integer literal.
I will also talk about formal verification of correctness and of the constant-time property of some of the library's functions. I will discuss the "Software Analysis Workbench" (Galois Inc.), an open-source tool for proving equivalence between LLVM bitcode (compiled C of C++ code) and a specification in Cryptol, which is a high-level functional language targeted at describing cryptographic algorithms. Also, I will cover ct-verif (Almeida et al.), a tool for verifying that a particular function is constant-time. The takeaway here is that nowadays there exist mature and easy-to-use open-source tools for fully-automatic formal verification.
