@article{7909, abstract = {Cell migration entails networks and bundles of actin filaments termed lamellipodia and microspikes or filopodia, respectively, as well as focal adhesions, all of which recruit Ena/VASP family members hitherto thought to antagonize efficient cell motility. However, we find these proteins to act as positive regulators of migration in different murine cell lines. CRISPR/Cas9-mediated loss of Ena/VASP proteins reduced lamellipodial actin assembly and perturbed lamellipodial architecture, as evidenced by changed network geometry as well as reduction of filament length and number that was accompanied by abnormal Arp2/3 complex and heterodimeric capping protein accumulation. Loss of Ena/VASP function also abolished the formation of microspikes normally embedded in lamellipodia, but not of filopodia capable of emanating without lamellipodia. Ena/VASP-deficiency also impaired integrin-mediated adhesion accompanied by reduced traction forces exerted through these structures. Our data thus uncover novel Ena/VASP functions of these actin polymerases that are fully consistent with their promotion of cell migration.}, author = {Damiano-Guercio, Julia and Kurzawa, Laëtitia and Müller, Jan and Dimchev, Georgi A and Schaks, Matthias and Nemethova, Maria and Pokrant, Thomas and Brühmann, Stefan and Linkner, Joern and Blanchoin, Laurent and Sixt, Michael K and Rottner, Klemens and Faix, Jan}, issn = {2050-084X}, journal = {eLife}, publisher = {eLife Sciences Publications}, title = {{Loss of Ena/VASP interferes with lamellipodium architecture, motility and integrin-dependent adhesion}}, doi = {10.7554/eLife.55351}, volume = {9}, year = {2020}, } @article{8669, abstract = {Pancreatic islets play an essential role in regulating blood glucose level. Although the molecular pathways underlying islet cell differentiation are beginning to be resolved, the cellular basis of islet morphogenesis and fate allocation remain unclear. By combining unbiased and targeted lineage tracing, we address the events leading to islet formation in the mouse. From the statistical analysis of clones induced at multiple embryonic timepoints, here we show that, during the secondary transition, islet formation involves the aggregation of multiple equipotent endocrine progenitors that transition from a phase of stochastic amplification by cell division into a phase of sublineage restriction and limited islet fission. Together, these results explain quantitatively the heterogeneous size distribution and degree of polyclonality of maturing islets, as well as dispersion of progenitors within and between islets. Further, our results show that, during the secondary transition, α- and β-cells are generated in a contemporary manner. Together, these findings provide insight into the cellular basis of islet development.}, author = {Sznurkowska, Magdalena K. and Hannezo, Edouard B and Azzarelli, Roberta and Chatzeli, Lemonia and Ikeda, Tatsuro and Yoshida, Shosei and Philpott, Anna and Simons, Benjamin D}, issn = {2041-1723}, journal = {Nature Communications}, publisher = {Springer Nature}, title = {{Tracing the cellular basis of islet specification in mouse pancreas}}, doi = {10.1038/s41467-020-18837-3}, volume = {11}, year = {2020}, } @article{8788, abstract = {We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically . We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically.}, author = {Pavlogiannis, Andreas and Schaumberger, Nico and Schmid, Ulrich and Chatterjee, Krishnendu}, issn = {1937-4151}, journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems}, number = {11}, pages = {3981--3992}, publisher = {IEEE}, title = {{Precedence-aware automated competitive analysis of real-time scheduling}}, doi = {10.1109/TCAD.2020.3012803}, volume = {39}, year = {2020}, } @article{7563, abstract = {We introduce “state space persistence analysis” for deducing the symbolic dynamics of time series data obtained from high-dimensional chaotic attractors. To this end, we adapt a topological data analysis technique known as persistent homology for the characterization of state space projections of chaotic trajectories and periodic orbits. By comparing the shapes along a chaotic trajectory to those of the periodic orbits, state space persistence analysis quantifies the shape similarity of chaotic trajectory segments and periodic orbits. We demonstrate the method by applying it to the three-dimensional Rössler system and a 30-dimensional discretization of the Kuramoto–Sivashinsky partial differential equation in (1+1) dimensions. One way of studying chaotic attractors systematically is through their symbolic dynamics, in which one partitions the state space into qualitatively different regions and assigns a symbol to each such region.1–3 This yields a “coarse-grained” state space of the system, which can then be reduced to a Markov chain encoding all possible transitions between the states of the system. While it is possible to obtain the symbolic dynamics of low-dimensional chaotic systems with standard tools such as Poincaré maps, when applied to high-dimensional systems such as turbulent flows, these tools alone are not sufficient to determine symbolic dynamics.4,5 In this paper, we develop “state space persistence analysis” and demonstrate that it can be utilized to infer the symbolic dynamics in very high-dimensional settings.}, author = {Yalniz, Gökhan and Budanur, Nazmi B}, issn = {1089-7682}, journal = {Chaos}, number = {3}, publisher = {AIP Publishing}, title = {{Inferring symbolic dynamics of chaotic flows from persistence}}, doi = {10.1063/1.5122969}, volume = {30}, year = {2020}, } @inproceedings{8135, abstract = {Discrete Morse theory has recently lead to new developments in the theory of random geometric complexes. This article surveys the methods and results obtained with this new approach, and discusses some of its shortcomings. It uses simulations to illustrate the results and to form conjectures, getting numerical estimates for combinatorial, topological, and geometric properties of weighted and unweighted Delaunay mosaics, their dual Voronoi tessellations, and the Alpha and Wrap complexes contained in the mosaics.}, author = {Edelsbrunner, Herbert and Nikitenko, Anton and Ölsböck, Katharina and Synak, Peter}, booktitle = {Topological Data Analysis}, isbn = {9783030434076}, issn = {2197-8549}, pages = {181--218}, publisher = {Springer Nature}, title = {{Radius functions on Poisson–Delaunay mosaics and related complexes experimentally}}, doi = {10.1007/978-3-030-43408-3_8}, volume = {15}, year = {2020}, } @article{8705, abstract = {We consider the quantum mechanical many-body problem of a single impurity particle immersed in a weakly interacting Bose gas. The impurity interacts with the bosons via a two-body potential. We study the Hamiltonian of this system in the mean-field limit and rigorously show that, at low energies, the problem is well described by the Fröhlich polaron model.}, author = {Mysliwy, Krzysztof and Seiringer, Robert}, issn = {1424-0637}, journal = {Annales Henri Poincare}, number = {12}, pages = {4003--4025}, publisher = {Springer Nature}, title = {{Microscopic derivation of the Fröhlich Hamiltonian for the Bose polaron in the mean-field limit}}, doi = {10.1007/s00023-020-00969-3}, volume = {21}, year = {2020}, } @phdthesis{7944, abstract = {This thesis considers two examples of reconfiguration problems: flipping edges in edge-labelled triangulations of planar point sets and swapping labelled tokens placed on vertices of a graph. In both cases the studied structures – all the triangulations of a given point set or all token placements on a given graph – can be thought of as vertices of the so-called reconfiguration graph, in which two vertices are adjacent if the corresponding structures differ by a single elementary operation – by a flip of a diagonal in a triangulation or by a swap of tokens on adjacent vertices, respectively. We study the reconfiguration of one instance of a structure into another via (shortest) paths in the reconfiguration graph. For triangulations of point sets in which each edge has a unique label and a flip transfers the label from the removed edge to the new edge, we prove a polynomial-time testable condition, called the Orbit Theorem, that characterizes when two triangulations of the same point set lie in the same connected component of the reconfiguration graph. The condition was first conjectured by Bose, Lubiw, Pathak and Verdonschot. We additionally provide a polynomial time algorithm that computes a reconfiguring flip sequence, if it exists. Our proof of the Orbit Theorem uses topological properties of a certain high-dimensional cell complex that has the usual reconfiguration graph as its 1-skeleton. In the context of token swapping on a tree graph, we make partial progress on the problem of finding shortest reconfiguration sequences. We disprove the so-called Happy Leaf Conjecture and demonstrate the importance of swapping tokens that are already placed at the correct vertices. We also prove that a generalization of the problem to weighted coloured token swapping is NP-hard on trees but solvable in polynomial time on paths and stars.}, author = {Masárová, Zuzana}, isbn = {978-3-99078-005-3}, issn = {2663-337X}, keywords = {reconfiguration, reconfiguration graph, triangulations, flip, constrained triangulations, shellability, piecewise-linear balls, token swapping, trees, coloured weighted token swapping}, pages = {160}, publisher = {Institute of Science and Technology Austria}, title = {{Reconfiguration problems}}, doi = {10.15479/AT:ISTA:7944}, year = {2020}, } @phdthesis{8574, abstract = {This thesis concerns itself with the interactions of evolutionary and ecological forces and the consequences on genetic diversity and the ultimate survival of populations. It is important to understand what signals processes leave on the genome and what we can infer from such data, which is usually abundant but noisy. Furthermore, understanding how and when populations adapt or go extinct is important for practical purposes, such as the genetic management of populations, as well as for theoretical questions, since local adaptation can be the first step toward speciation. In Chapter 2, we introduce the method of maximum entropy to approximate the demographic changes of a population in a simple setting, namely the logistic growth model with immigration. We show that this method is not only a powerful tool in physics but can be gainfully applied in an ecological framework. We investigate how well it approximates the real behavior of the system, and find that is does so, even in unexpected situations. Finally, we illustrate how it can model changing environments. In Chapter 3, we analyze the co-evolution of allele frequencies and population sizes in an infinite island model. We give conditions under which polygenic adaptation to a rare habitat is possible. The model we use is based on the diffusion approximation, considers eco-evolutionary feedback mechanisms (hard selection), and treats both drift and environmental fluctuations explicitly. We also look at limiting scenarios, for which we derive analytical expressions. In Chapter 4, we present a coalescent based simulation tool to obtain patterns of diversity in a spatially explicit subdivided population, in which the demographic history of each subpopulation can be specified. We compare the results to existing predictions, and explore the relative importance of time and space under a variety of spatial arrangements and demographic histories, such as expansion and extinction. In the last chapter, we give a brief outlook to further research. }, author = {Szep, Eniko}, issn = {2663-337X}, pages = {158}, publisher = {Institute of Science and Technology Austria}, title = {{Local adaptation in metapopulations}}, doi = {10.15479/AT:ISTA:8574}, year = {2020}, } @phdthesis{8032, abstract = {Algorithms in computational 3-manifold topology typically take a triangulation as an input and return topological information about the underlying 3-manifold. However, extracting the desired information from a triangulation (e.g., evaluating an invariant) is often computationally very expensive. In recent years this complexity barrier has been successfully tackled in some cases by importing ideas from the theory of parameterized algorithms into the realm of 3-manifolds. Various computationally hard problems were shown to be efficiently solvable for input triangulations that are sufficiently “tree-like.” In this thesis we focus on the key combinatorial parameter in the above context: we consider the treewidth of a compact, orientable 3-manifold, i.e., the smallest treewidth of the dual graph of any triangulation thereof. By building on the work of Scharlemann–Thompson and Scharlemann–Schultens–Saito on generalized Heegaard splittings, and on the work of Jaco–Rubinstein on layered triangulations, we establish quantitative relations between the treewidth and classical topological invariants of a 3-manifold. In particular, among other results, we show that the treewidth of a closed, orientable, irreducible, non-Haken 3-manifold is always within a constant factor of its Heegaard genus.}, author = {Huszár, Kristóf}, isbn = {978-3-99078-006-0}, issn = {2663-337X}, pages = {xviii+120}, publisher = {Institute of Science and Technology Austria}, title = {{Combinatorial width parameters for 3-dimensional manifolds}}, doi = {10.15479/AT:ISTA:8032}, year = {2020}, } @inproceedings{8195, abstract = {This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier.}, author = {Kragl, Bernhard and Qadeer, Shaz and Henzinger, Thomas A}, booktitle = {Computer Aided Verification}, isbn = {9783030532871}, issn = {1611-3349}, pages = {275--298}, publisher = {Springer Nature}, title = {{Refinement for structured concurrent programs}}, doi = {10.1007/978-3-030-53288-8_14}, volume = {12224}, year = {2020}, } @phdthesis{8589, abstract = {The plant hormone auxin plays indispensable roles in plant growth and development. An essential level of regulation in auxin action is the directional auxin transport within cells. The establishment of auxin gradient in plant tissue has been attributed to local auxin biosynthesis and directional intercellular auxin transport, which both are controlled by various environmental and developmental signals. It is well established that asymmetric auxin distribution in cells is achieved by polarly localized PIN-FORMED (PIN) auxin efflux transporters. Despite the initial insights into cellular mechanisms of PIN polarization obtained from the last decades, the molecular mechanism and specific regulators mediating PIN polarization remains elusive. In this thesis, we aim to find novel players in PIN subcellular polarity regulation during Arabidopsis development. We first characterize the physiological effect of piperonylic acid (PA) on Arabidopsis hypocotyl gravitropic bending and PIN polarization. Secondly, we reveal the importance of SCFTIR1/AFB auxin signaling pathway in shoot gravitropism bending termination. In addition, we also explore the role of myosin XI complex, and actin cytoskeleton in auxin feedback regulation on PIN polarity. In Chapter 1, we give an overview of the current knowledge about PIN-mediated auxin fluxes in various plant tropic responses. In Chapter 2, we study the physiological effect of PA on shoot gravitropic bending. Our results show that PA treatment inhibits auxin-mediated PIN3 repolarization by interfering with PINOID and PIN3 phosphorylation status, ultimately leading to hyperbending hypocotyls. In Chapter 3, we provide evidence to show that the SCFTIR1/AFB nuclear auxin signaling pathway is crucial and required for auxin-mediated PIN3 repolarization and shoot gravitropic bending termination. In Chapter 4, we perform a phosphoproteomics approach and identify the motor protein Myosin XI and its binding protein, the MadB2 family, as an essential regulator of PIN polarity for auxin-canalization related developmental processes. In Chapter 5, we demonstrate the vital role of actin cytoskeleton in auxin feedback on PIN polarity by regulating PIN subcellular trafficking. Overall, the data presented in this PhD thesis brings novel insights into the PIN polar localization regulation that resulted in the (re)establishment of the polar auxin flow and gradient in response to environmental stimuli during plant development.}, author = {Han, Huibin}, issn = {2663-337X}, pages = {164}, publisher = {Institute of Science and Technology Austria}, title = {{Novel insights into PIN polarity regulation during Arabidopsis development}}, doi = {10.15479/AT:ISTA:8589}, year = {2020}, } @phdthesis{8366, abstract = {Fabrication of curved shells plays an important role in modern design, industry, and science. Among their remarkable properties are, for example, aesthetics of organic shapes, ability to evenly distribute loads, or efficient flow separation. They find applications across vast length scales ranging from sky-scraper architecture to microscopic devices. But, at the same time, the design of curved shells and their manufacturing process pose a variety of challenges. In this thesis, they are addressed from several perspectives. In particular, this thesis presents approaches based on the transformation of initially flat sheets into the target curved surfaces. This involves problems of interactive design of shells with nontrivial mechanical constraints, inverse design of complex structural materials, and data-driven modeling of delicate and time-dependent physical properties. At the same time, two newly-developed self-morphing mechanisms targeting flat-to-curved transformation are presented. In architecture, doubly curved surfaces can be realized as cold bent glass panelizations. Originally flat glass panels are bent into frames and remain stressed. This is a cost-efficient fabrication approach compared to hot bending, when glass panels are shaped plastically. However such constructions are prone to breaking during bending, and it is highly nontrivial to navigate the design space, keeping the panels fabricable and aesthetically pleasing at the same time. We introduce an interactive design system for cold bent glass façades, while previously even offline optimization for such scenarios has not been sufficiently developed. Our method is based on a deep learning approach providing quick and high precision estimation of glass panel shape and stress while handling the shape multimodality. Fabrication of smaller objects of scales below 1 m, can also greatly benefit from shaping originally flat sheets. In this respect, we designed new self-morphing shell mechanisms transforming from an initial flat state to a doubly curved state with high precision and detail. Our so-called CurveUps demonstrate the encodement of the geometric information into the shell. Furthermore, we explored the frontiers of programmable materials and showed how temporal information can additionally be encoded into a flat shell. This allows prescribing deformation sequences for doubly curved surfaces and, thus, facilitates self-collision avoidance enabling complex shapes and functionalities otherwise impossible. Both of these methods include inverse design tools keeping the user in the design loop.}, author = {Guseinov, Ruslan}, isbn = {978-3-99078-010-7}, issn = {2663-337X}, keywords = {computer-aided design, shape modeling, self-morphing, mechanical engineering}, pages = {118}, publisher = {Institute of Science and Technology Austria}, title = {{Computational design of curved thin shells: From glass façades to programmable matter}}, doi = {10.15479/AT:ISTA:8366}, year = {2020}, } @phdthesis{8358, abstract = {During bacterial cell division, the tubulin-homolog FtsZ forms a ring-like structure at the center of the cell. This so-called Z-ring acts as a scaffold recruiting several division-related proteins to mid-cell and plays a key role in distributing proteins at the division site, a feature driven by the treadmilling motion of FtsZ filaments around the septum. What regulates the architecture, dynamics and stability of the Z-ring is still poorly understood, but FtsZ-associated proteins (Zaps) are known to play an important role. Advances in fluorescence microscopy and in vitro reconstitution experiments have helped to shed light into some of the dynamic properties of these complex systems, but methods that allow to collect and analyze large quantitative data sets of the underlying polymer dynamics are still missing. Here, using an in vitro reconstitution approach, we studied how different Zaps affect FtsZ filament dynamics and organization into large-scale patterns, giving special emphasis to the role of the well-conserved protein ZapA. For this purpose, we use high-resolution fluorescence microscopy combined with novel image analysis workfows to study pattern organization and polymerization dynamics of active filaments. We quantified the influence of Zaps on FtsZ on three diferent spatial scales: the large-scale organization of the membrane-bound filament network, the underlying polymerization dynamics and the behavior of single molecules. We found that ZapA cooperatively increases the spatial order of the filament network, binds only transiently to FtsZ filaments and has no effect on filament length and treadmilling velocity. Our data provides a model for how FtsZ-associated proteins can increase the precision and stability of the bacterial cell division machinery in a switch-like manner, without compromising filament dynamics. Furthermore, we believe that our automated quantitative methods can be used to analyze a large variety of dynamic cytoskeletal systems, using standard time-lapse movies of homogeneously labeled proteins obtained from experiments in vitro or even inside the living cell. }, author = {Dos Santos Caldas, Paulo R}, isbn = {978-3-99078-009-1}, issn = {2663-337X}, pages = {135}, publisher = {Institute of Science and Technology Austria}, title = {{Organization and dynamics of treadmilling filaments in cytoskeletal networks of FtsZ and its crosslinkers}}, doi = {10.15479/AT:ISTA:8358}, year = {2020}, } @phdthesis{8390, abstract = {Deep neural networks have established a new standard for data-dependent feature extraction pipelines in the Computer Vision literature. Despite their remarkable performance in the standard supervised learning scenario, i.e. when models are trained with labeled data and tested on samples that follow a similar distribution, neural networks have been shown to struggle with more advanced generalization abilities, such as transferring knowledge across visually different domains, or generalizing to new unseen combinations of known concepts. In this thesis we argue that, in contrast to the usual black-box behavior of neural networks, leveraging more structured internal representations is a promising direction for tackling such problems. In particular, we focus on two forms of structure. First, we tackle modularity: We show that (i) compositional architectures are a natural tool for modeling reasoning tasks, in that they efficiently capture their combinatorial nature, which is key for generalizing beyond the compositions seen during training. We investigate how to to learn such models, both formally and experimentally, for the task of abstract visual reasoning. Then, we show that (ii) in some settings, modularity allows us to efficiently break down complex tasks into smaller, easier, modules, thereby improving computational efficiency; We study this behavior in the context of generative models for colorization, as well as for small objects detection. Secondly, we investigate the inherently layered structure of representations learned by neural networks, and analyze its role in the context of transfer learning and domain adaptation across visually dissimilar domains. }, author = {Royer, Amélie}, isbn = {978-3-99078-007-7}, issn = {2663-337X}, pages = {197}, publisher = {Institute of Science and Technology Austria}, title = {{Leveraging structure in Computer Vision tasks for flexible Deep Learning models}}, doi = {10.15479/AT:ISTA:8390}, year = {2020}, } @inbook{8092, abstract = {Image translation refers to the task of mapping images from a visual domain to another. Given two unpaired collections of images, we aim to learn a mapping between the corpus-level style of each collection, while preserving semantic content shared across the two domains. We introduce xgan, a dual adversarial auto-encoder, which captures a shared representation of the common domain semantic content in an unsupervised way, while jointly learning the domain-to-domain image translations in both directions. We exploit ideas from the domain adaptation literature and define a semantic consistency loss which encourages the learned embedding to preserve semantics shared across domains. We report promising qualitative results for the task of face-to-cartoon translation. The cartoon dataset we collected for this purpose, “CartoonSet”, is also publicly available as a new benchmark for semantic style transfer at https://google.github.io/cartoonset/index.html.}, author = {Royer, Amélie and Bousmalis, Konstantinos and Gouws, Stephan and Bertsch, Fred and Mosseri, Inbar and Cole, Forrester and Murphy, Kevin}, booktitle = {Domain Adaptation for Visual Understanding}, editor = {Singh, Richa and Vatsa, Mayank and Patel, Vishal M. and Ratha, Nalini}, isbn = {9783030306717}, pages = {33--49}, publisher = {Springer Nature}, title = {{XGAN: Unsupervised image-to-image translation for many-to-many mappings}}, doi = {10.1007/978-3-030-30671-7_3}, year = {2020}, } @inproceedings{8272, abstract = {We study turn-based stochastic zero-sum games with lexicographic preferences over reachability and safety objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as angelic and demonic non-determinism. Lexicographic order allows to consider multiple objectives with a strict preference order over the satisfaction of the objectives. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. We establish determinacy of such games and present strategy and computational complexity results. For strategy complexity, we show that lexicographically optimal strategies exist that are deterministic and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP∩coNP , matching the current known bound for single objectives; and in general the decision problem is PSPACE -hard and can be solved in NEXPTIME∩coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to computation of optimal strategies in a sequence of single-objectives games. We have implemented our algorithm and report experimental results on various case studies.}, author = {Chatterjee, Krishnendu and Katoen, Joost P and Weininger, Maximilian and Winkler, Tobias}, booktitle = {International Conference on Computer Aided Verification}, isbn = {9783030532901}, issn = {1611-3349}, pages = {398--420}, publisher = {Springer Nature}, title = {{Stochastic games with lexicographic reachability-safety objectives}}, doi = {10.1007/978-3-030-53291-8_21}, volume = {12225}, year = {2020}, } @inproceedings{8339, abstract = {Discrete Gaussian distributions over lattices are central to lattice-based cryptography, and to the computational and mathematical aspects of lattices more broadly. The literature contains a wealth of useful theorems about the behavior of discrete Gaussians under convolutions and related operations. Yet despite their structural similarities, most of these theorems are formally incomparable, and their proofs tend to be monolithic and written nearly “from scratch,” making them unnecessarily hard to verify, understand, and extend. In this work we present a modular framework for analyzing linear operations on discrete Gaussian distributions. The framework abstracts away the particulars of Gaussians, and usually reduces proofs to the choice of appropriate linear transformations and elementary linear algebra. To showcase the approach, we establish several general properties of discrete Gaussians, and show how to obtain all prior convolution theorems (along with some new ones) as straightforward corollaries. As another application, we describe a self-reduction for Learning With Errors (LWE) that uses a fixed number of samples to generate an unlimited number of additional ones (having somewhat larger error). The distinguishing features of our reduction are its simple analysis in our framework, and its exclusive use of discrete Gaussians without any loss in parameters relative to a prior mixed discrete-and-continuous approach. As a contribution of independent interest, for subgaussian random matrices we prove a singular value concentration bound with explicitly stated constants, and we give tighter heuristics for specific distributions that are commonly used for generating lattice trapdoors. These bounds yield improvements in the concrete bit-security estimates for trapdoor lattice cryptosystems.}, author = {Genise, Nicholas and Micciancio, Daniele and Peikert, Chris and Walter, Michael}, booktitle = {23rd IACR International Conference on the Practice and Theory of Public-Key Cryptography}, isbn = {9783030453732}, issn = {1611-3349}, location = {Edinburgh, United Kingdom}, pages = {623--651}, publisher = {Springer Nature}, title = {{Improved discrete Gaussian and subgaussian analysis for lattice cryptography}}, doi = {10.1007/978-3-030-45374-9_21}, volume = {12110}, year = {2020}, } @inproceedings{8987, abstract = {Currently several projects aim at designing and implementing protocols for privacy preserving automated contact tracing to help fight the current pandemic. Those proposal are quite similar, and in their most basic form basically propose an app for mobile phones which broadcasts frequently changing pseudorandom identifiers via (low energy) Bluetooth, and at the same time, the app stores IDs broadcast by phones in its proximity. Only if a user is tested positive, they upload either the beacons they did broadcast (which is the case in decentralized proposals as DP-3T, east and west coast PACT or Covid watch) or received (as in Popp-PT or ROBERT) during the last two weeks or so. Vaudenay [eprint 2020/399] observes that this basic scheme (he considers the DP-3T proposal) succumbs to relay and even replay attacks, and proposes more complex interactive schemes which prevent those attacks without giving up too many privacy aspects. Unfortunately interaction is problematic for this application for efficiency and security reasons. The countermeasures that have been suggested so far are either not practical or give up on key privacy aspects. We propose a simple non-interactive variant of the basic protocol that (security) Provably prevents replay and (if location data is available) relay attacks. (privacy) The data of all parties (even jointly) reveals no information on the location or time where encounters happened. (efficiency) The broadcasted message can fit into 128 bits and uses only basic crypto (commitments and secret key authentication). Towards this end we introduce the concept of “delayed authentication”, which basically is a message authentication code where verification can be done in two steps, where the first doesn’t require the key, and the second doesn’t require the message.}, author = {Pietrzak, Krzysztof Z}, booktitle = {Progress in Cryptology}, isbn = {9783030652760}, issn = {1611-3349}, location = {Bangalore, India}, pages = {3--15}, publisher = {Springer Nature}, title = {{Delayed authentication: Preventing replay and relay attacks in private contact tracing}}, doi = {10.1007/978-3-030-65277-7_1}, volume = {12578}, year = {2020}, } @inproceedings{8322, abstract = {Reverse firewalls were introduced at Eurocrypt 2015 by Miro-nov and Stephens-Davidowitz, as a method for protecting cryptographic protocols against attacks on the devices of the honest parties. In a nutshell: a reverse firewall is placed outside of a device and its goal is to “sanitize” the messages sent by it, in such a way that a malicious device cannot leak its secrets to the outside world. It is typically assumed that the cryptographic devices are attacked in a “functionality-preserving way” (i.e. informally speaking, the functionality of the protocol remains unchanged under this attacks). In their paper, Mironov and Stephens-Davidowitz construct a protocol for passively-secure two-party computations with firewalls, leaving extension of this result to stronger models as an open question. In this paper, we address this problem by constructing a protocol for secure computation with firewalls that has two main advantages over the original protocol from Eurocrypt 2015. Firstly, it is a multiparty computation protocol (i.e. it works for an arbitrary number n of the parties, and not just for 2). Secondly, it is secure in much stronger corruption settings, namely in the active corruption model. More precisely: we consider an adversary that can fully corrupt up to 𝑛−1 parties, while the remaining parties are corrupt in a functionality-preserving way. Our core techniques are: malleable commitments and malleable non-interactive zero-knowledge, which in particular allow us to create a novel protocol for multiparty augmented coin-tossing into the well with reverse firewalls (that is based on a protocol of Lindell from Crypto 2001).}, author = {Chakraborty, Suvradip and Dziembowski, Stefan and Nielsen, Jesper Buus}, booktitle = {Advances in Cryptology – CRYPTO 2020}, isbn = {9783030568795}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {732--762}, publisher = {Springer Nature}, title = {{Reverse firewalls for actively secure MPCs}}, doi = {10.1007/978-3-030-56880-1_26}, volume = {12171}, year = {2020}, } @inproceedings{8194, abstract = {Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.}, author = {Baranowski, Marek and He, Shaobo and Lechner, Mathias and Nguyen, Thanh Son and Rakamarić, Zvonimir}, booktitle = {Automated Reasoning}, isbn = {9783030510732}, issn = {1611-3349}, location = {Paris, France}, pages = {13--31}, publisher = {Springer Nature}, title = {{An SMT theory of fixed-point arithmetic}}, doi = {10.1007/978-3-030-51074-9_2}, volume = {12166}, year = {2020}, }