SearcharxivSearch

arXiv subjects

Daniel Lehmann

Publications and source records attributed to Daniel Lehmann.

At least 19 recordsLinked to original sources

Execution-Aware Program Reduction for WebAssembly via Record and Replay

WebAssembly (Wasm) programs may trigger bugs in their engine implementations. To aid debugging, program reduction techniques try to produce a smaller variant of the input program that still triggers the bug. However, existing execution-unaware program reduction techniques struggle with large and complex Wasm programs, because they rely on static information and apply syntactic transformations, while ignoring the valuable information offered by the input program's execution behavior. We present RR-Reduce and Hybrid-Reduce, novel execution-aware program reduction techniques that leverage execution behaviors via record and replay. RR-Reduce identifies a bug-triggering function as the target function, isolates that function from the rest of the program, and generates a reduced program that replays only the interactions between the target function and the rest of the program. Hybrid-Reduce combines a complementary execution-unaware reduction technique with RR-Reduce to further reduce program size. We evaluate RR-Reduce and Hybrid-Reduce on 28 Wasm programs that trigger a diverse set of bugs in three engines. On average, RR-Reduce reduces the programs to 1.20 percent of their original size in 14.5 minutes, which outperforms the state of the art by 33.15 times in terms of reduction time. Hybrid-Reduce reduces the programs to 0.13 percent of their original size in 3.5 hours, which outperforms the state of the art by 3.42 times in terms of reduced program size and 2.26 times in terms of reduction time. We envision RR-Reduce as the go-to tool for rapid, on-demand debugging in minutes, and Hybrid-Reduce for scenarios where developers require the smallest possible programs.

cs.PL

Ordinary and calibrated differential operators Application to curvilinear webs

We study the space of the solutions $s$ of any system of partial differential equations $ D(j^ks)=0 $ defined by a linear and homogeneous differential operator $ D:J^kE\to F $ of any order $k\geq 1$, which is ``ordinary" (i.e. which is generic in some sense among all $D$'s), $E$ and $F$ being vector bundles over a $n$-dimensional manifold $V$, and $D$ being assumed to be surjective at any point of $V$. In some range of the ranks $p$ and $q$ of these bundles ($p < q\leq np$ in the case $k=1$), we first give an upper-bound $\pi(n,k,p,q)$ for the dimension of the space ${\mathcal S}_m$ of the germs of solutions at a generic point $m$ of the ambiant manifold. If these ranks satisfy moreover to some condition of integrality (in the case $k=1$, $\frac{p(n-1)}{q-p}$ must be an integer), and we then say that $D$ is ``calibrated", we build a vector bundle $\mathcal E$ of rank $\pi(n,k,p,q)$ on $V$, provided with a tautological connection $\nabla$, whose curvature is an obstruction for the dimension of ${\mathcal S}_m$ to reach its maximal value. We also prove a ``theorem of concentration'' : relatively to some convenient trivialization of $\mathcal E$, some coefficients of this curvature vanish systematically. As an example, we provide, for any curvilinear $d$-web on $V$, a differential operator $D$ of order one, which is always ordinary and calibrated, and for which ${\mathcal S}_m$ is the space of germs of abelian relations ([L]). Thus, we recover the Damiano's upper-bound ([D1]) for the rank of such a web, and we can define in the most general case the ``curvature'' of such a web, already known for $n=2$ (see [BB] if $d=3$, and [Pa],[H1],[Pi1] for arbitrary $d$), obstruction for this rank to be maximum.

math.DG

Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks

WebAssembly (Wasm for short) brings a new, powerful capability to the web as well as Edge, IoT, and embedded systems. Wasm is a portable, compact binary code format with high performance and robust sandboxing properties. As Wasm applications grow in size and importance, the complex performance characteristics of diverse Wasm engines demand robust, representative benchmarks for proper tuning. Stopgap benchmark suites, such as PolyBenchC and libsodium, continue to be used in the literature, though they are known to be unrepresentative. Porting of more complex suites remains difficult because Wasm lacks many system APIs and extracting real-world Wasm benchmarks from the web is difficult due to complex host interactions. To address this challenge, we introduce Wasm-R3, the first record and replay technique for Wasm. Wasm-R3 transparently injects instrumentation into Wasm modules to record an execution trace from inside the module, then reduces the execution trace via several optimizations, and finally produces a replay module that is executable sandalone without any host environment - on any engine. The benchmarks created by our approach are (i) realistic, because the approach records real-world web applications, (ii) faithful to the original execution, because the replay benchmark includes the unmodified original code, only adding emulation of host interactions, and (iii) standalone, because the replay benchmarks run on any engine. Applying Wasm-R3 to web-based Wasm applications in the wild demonstrates the correctness of our approach as well as the effectiveness of our optimizations, which reduce the recorded traces by 99.53 percent and the size of the replay benchmark by 9.98 percent. We release the resulting benchmark suite of 27 applications, called Wasm-R3-Bench, to the community, to inspire a new generation of realistic and standalone Wasm benchmarks.

cs.PL

Projection-algebras and quantum logic

P-algebras are a non-commutative, non-associative generalization of Boolean algebras that are for quantum logic what Boolean algebras are for classical logic. P-algebras have type where 0 is a constant, ' is unary and . is binary. Elements of X are called features. A partial order is defined on the set X of features by x <= y iff x.y = x. Features commute, i.e., x.y = y.x iff x.y <= x. Features x and y are said to be orthogonal iff x.y = 0 and orthogonality is a symmetric relation.The operation + is defined as the dual of . and it is commutative on orthogonal features. The closed subspaces of a separable Hilbert space form a P-algebra under orthogonal complementation and projection of a subspace onto another one.P-algebras are complemented orthomodular posets but they are not lattices. Existence of least upper bounds for ascending sequences is equivalent to the existence of least upper bounds for countable sets of pairwise orthogonal elements. Atomic algebras are defined and their main properties are studied. The logic of P-algebras is then completely characterized. The language contains a unary connective corresponding to the operation ' and a binary connective corresponding to the operation ".". It is a substructural logic of sequents where the Exchange rule is extremely limited. It is proved to be sound and complete for P-algebras.

quant-ph

Foundations of non-commutative probability theory (Extended abstract)

Kolmogorov's setting for probability theory is given an original generalization to account for probabilities arising from Quantum Mechanics. The sample space has a central role in this presentation and random variables, i.e., observables, are defined in a natural way.The mystery presented by the algebraic equations satisfied by (non-commuting) observables that cannot be observed in the same states is elucidated.

quant-ph

A substructural logic for quantum measurements

This paper presents a substructural logic of sequents with very restricted exchange and weakening rules. It is sound with respect to sequences of measurements of a quantic system. A sound and complete semantics is provided. The semantic structures include a binary relation that expresses orthogonality between elements and enables the definition of an operation that generalizes the projection operation in Hilbert spaces. The language has a unitary connective, a sort of negation, and two dual binary connectives that are neither commutative nor associative, sorts of conjunction and disjunction. This provides a logic for quantum measurements whose proof theory is aesthetically pleasing.

quant-ph

Etude des (n+1)-tissus de courbes en dimension n

For $(n+1)$-webs by curves in an ambiant $n$-dimensional manifold, we first define a generalization of the well known Blaschke curvature of the dimension two, which vanishes iff the web has the maximum possible rank which is one. But, contrary to the dimension two where all 3-webs of rank one are locally isomorphic, we prove that there are infinitely many classes of isomorphism for germs of 4-webs by curves of rank one in the dimension three : we provide a procedure for building all of them, up to isomorphism, and give examples of invariants of these classes allowing in particular to distinguish the so-called quadrilateral webs among them.

math.DG

Le rang des tissus de Nakai

According to Alain Hénaut, a planar 4-web is called Nakai's web if the cross-ratio of the tangents to the four foliations at each point is constant and if it has no hexagonal 3-subweb. We prove that Nakai's webs have rank 0 or 1. We give examples with rank 1 and present a universal way to build such examples.

math.DG

Non-associative and projective linear logics

A non-commutative, non-associative weakening of Girard's linear logic is developed for multiplicative and additive connectives. Additional assumptions capture the logic of quantic measurements.

cs.LO

Relations abéliennes des tissus ordinaires de codimension arbitraire

We generalize to webs of any codimension results already known in codimension one. Given a holomorphic $d$-web $\cal W$ of codimension $q$ $(q\leq n-1)$ in an ambiant $n$-dimensional holomorphic manifold $U$, we define for any integer $p$ $(1\leq p\leq q)$ the condition for such a web to be \emph{$p$-ordinary} $($resp. \emph{strongly $p$-ordinary}$)$. If this condition is satisfied, we then prove that its $p$-rank $r_p({\cal W})$ $\bigl($resp. its closed $p$-rank $\widetilde r_p({\cal W})\bigr)$, i.e. the maximal dimension of the vector space of the germs of $p$-abelian relations $($resp. of closed $p$-abelian relations$)$ at a point $m$ of $U$, is finite. We then give an upper-bound $π_p^0(n,d,q)$ $\bigl($resp. $π'_p(n,d,q)\bigr)$ for these ranks. Moreover, for some values of $d$, and we then say then that the web is \emph{$p$-calibrated} $($resp. \emph{strongly $p$-calibrated}$)$, we define a tautological holomorphic connection on a holomorphic vector bundle of rank $π_p^0(n,d,q)$ $\bigl($resp. $π'_p(n,d,q)\bigr)$, for which the sections with vanishing covariant derivative may be identified with $p$-abelian relations $($resp. closed $p$-abelian relations$)$. The curvature of this connection is then an obstruction for the rank $r_p({\cal W})$ $\bigl($resp. $\widetilde r_p({\cal W})\bigr)$ to be maximal. The main change is the correction of a mistake $($proposition 4, section 6-5$)$ in the first version : the 1-rank of the concerned web is not 0 as we claimed, but 1. However, the important corollary remains true : even at the level of germs, some 2-abelian relation exhibited by Goldberg in $ [G]$ on some web of codimension 2 in an ambiant space of dimension 4, is the coboundary of none 1-abelian relation. The section 7, devoted to this correction, is self content, not depending on the previous results of the paper.

math.DG

Fuzzm: Finding Memory Bugs through Binary-Only Instrumentation and Fuzzing of WebAssembly

WebAssembly binaries are often compiled from memory-unsafe languages, such as C and C++. Because of WebAssembly's linear memory and missing protection features, e.g., stack canaries, source-level memory vulnerabilities are exploitable in compiled WebAssembly binaries, sometimes even more easily than in native code. This paper addresses the problem of detecting such vulnerabilities through the first binary-only fuzzer for WebAssembly. Our approach, called Fuzzm, combines canary instrumentation to detect overflows and underflows on the stack and the heap, an efficient coverage instrumentation, a WebAssembly VM, and the input generation algorithm of the popular AFL fuzzer. Besides as an oracle for fuzzing, our canaries also serve as a stand-alone binary hardening technique to prevent the exploitation of vulnerable binaries in production. We evaluate Fuzzm with 28 real-world WebAssembly binaries, some compiled from source and some found in the wild without source code. The fuzzer explores thousands of execution paths, triggers dozens of crashes, and performs hundreds of program executions per second. When used for binary hardening, the approach prevents previously published exploits against vulnerable WebAssembly binaries while imposing low runtime overhead.

cs.CR

Courbes ordinaires de genre maximal

The ordinary algebraic curves of maximal rank are also the arithmetically Cohen-Maccaulay curves of minimal rank. We give sufficient conditions for such curves to exist as well as examples, generalizing results of [GHL] in the dimension three.

math.AG

Revealed Preferences for Matching with Contracts

Many-to-many matching with contracts is studied in the framework of revealed preferences. All preferences are described by choice functions that satisfy natural conditions. Under a no-externality assumption individual preferences can be aggregated into a single choice function expressing a collective preference. In this framework, a two-sided matching problem may be described as an agreement problem between two parties: the two parties must find a stable agreement, i.e., a set of contracts from which no party will want to take away any contract and to which the two parties cannot agree to add any contract. On such stable agreements each party's preference relation is a partial order and the two parties have inverse preferences. An algorithm is presented that generalizes algorithms previously proposed in less general situations. This algorithm provides a stable agreement that is preferred to all stable agreements by one of the parties and therefore less preferred than all stable agreements by the other party. The number of steps of the algorithm is linear in the size of the set of contracts, i.e., polynomial in the size of the problem. The algorithm provides a proof that stable agreements form a lattice under the two inverse preference relations. Under additional assumptions on the role of money in preferences, agreement problems can describe general two-sided markets in which goods are exchanged for money. Stable agreements provide a solution concept, including prices, that is more general than competitive equilibria. They satisfy an almost one price law for identical items.

cs.GT

Quality of local equilibria in discrete exchange economies

This paper defines the notion of a local equilibrium of quality $(r , s)$, $0 \leq r , s$, in a discrete exchange economy: a partial allocation and item prices that guarantee certain stability properties parametrized by the numbers $r$ and $s$. The quality $( r , s )$ measures the fit between the allocation and the prices: the larger $r$ and $s$ the closer the fit. For $r , s \leq 1$ this notion provides a graceful degradation for the conditional equilibria of [10] which are exactly the local equilibria of quality $( 1 , 1 )$. For $1 < r , s $ the local equilibria of quality $( r , s )$ are {\em more stable} than conditional equilibria. Any local equilibrium of quality $( r , s )$ provides, without any assumption on the type of the agents' valuations, an allocation whose value is at least $\frac{r s} { 1 + r s }$ the optimal fractional allocation. In any economy in which all agents' valuations are $a$-submodular, i.e., exhibit complementarity bounded by $a \: \geq \: 1$, there is a local equilibrium of quality $( \frac{1} {a} , \frac{1}{a} )$. In such an economy any greedy allocation provides a local equilibrium of quality $( 1 , \frac{1}{a} ) $. Walrasian equilibria are not amenable to such graceful degradation.

cs.GT

Ultra valuations

This paper proposes an original exchange property of valuations.This property is shown to be equivalent to a property described by Dress and Terhalle in the context of discrete optimization and matroids and shown there to characterize the valuations for which the demand oracle can be implemented by a greedy algorithm. The same exchange property is also equivalent to a property described independently by Reijnierse, van Gellekom and Potters and by Lehmann, Lehmann and Nisan and shown there to be satisfied by substitutes valuations. It studies the family of valuations that satisfy this exchange property, the ultra valuations. Any substitutes valuation is an ultra valuation, but ultra valuations may exhibit complementarities. Any symmetric valuation is an ultra valuation. Substitutes valuations are exactly the submodular ultra valuations. Ultra valuations define ultrametrics on the set of items. The maximum of an ultra valuation on $n$ items can be found in $O(n^2)$ steps. Finding an efficient allocation among ultra valuations is NP-hard.

cs.GT

Wasabi: A Framework for Dynamically Analyzing WebAssembly

WebAssembly is the new low-level language for the web and has now been implemented in all major browsers since over a year. To ensure the security, performance, and correctness of future web applications, there is a strong need for dynamic analysis tools for WebAssembly. Unfortunately, building such tools from scratch requires knowledge of low-level details of the language, and perhaps even its runtime environment. This paper presents Wasabi, the first general-purpose framework for dynamically analyzing WebAssembly. Wasabi provides an easy-to-use, high-level API that allows implementing heavyweight dynamic analyses that can monitor all low-level behavior. The approach is based on binary instrumentation, which inserts calls to analysis functions written in JavaScript into a WebAssembly binary. Wasabi addresses several unique challenges not present for other binary instrumentation tools, such as the problem of tracing type-polymorphic instructions with analysis functions that have a fixed type, which we address through an on-demand monomorphization of analysis calls. To control the overhead imposed by an analysis, Wasabi selectively instruments only those instructions relevant for the analysis. Our evaluation on compute-intensive benchmarks and real-world applications shows that Wasabi (i) faithfully preserves the original program behavior, (ii) imposes an overhead that is reasonable for heavyweight dynamic analysis (depending on the program and the analyzed instructions, between 1.02x and 163x), and (iii) makes it straightforward to implement various dynamic analyses, including instruction counting, call graph extraction, memory access tracing, and taint analysis.

cs.PL

Rank of ordinary webs in codimension one. An effective method

We are interested by holomorphic $d$-webs $W$ of codimension one in a complex $n$-dimensional manifold $M$. If they are ordinary, i.e. if they satisfy to some condition of genericity (whose precise definition is recalled), we proved in [CL] that their rank $ρ(W)$ is upper-bounded by a certain number $π'(n,d)\ \bigl($which, for $n\geq 3$, is stictly smaller than the Castelnuovo-Chern's bound $π(n,d)\bigr)$. In fact, denoting by $c(n,h)$ the dimension of the space of homogeneous polynomials of degree $h$ with $n$ unknowns, and by $h_0$ the integer such that $$c(n,h_0-1)<d\leq c(n,h_0),$$ $π'(n,d)$ is just the first number of a decreasing sequence of positive integers $$π'(n,d)=ρ_{h_0-2}\geq ρ_{h_0-1}\geq \cdots\geq ρ_{h}\geq ρ_{h+1}\geq\cdots\geq ρ_{\infty}=ρ(W)\geq 0 $$ becoming stationary equal to $ρ(W)$ after a finite number of steps. This sequence is an interesting invariant of the web, refining the data of the only rank. The method is effective : theoretically, we can compute $ρ_h$ for any given $h$ ; and, as soon as two consecutive such numbers are equal ($ρ_h=ρ_{h+1}, \ h\geq h_0-2$), we can construct a holomorphic vector bundle $R_h\to M$ of rank $ρ_h$, equipped with a tautological holomorphic connection $\nabla^h$ whose curvature $K^h$ vanishes iff the above sequence is stationary from there. Thus, we may stop the process at the first step where the curvature vanishes. Examples will be given.

math.DG