Showing 1–50 of 73 results for author: Stefan, D

Robust Constant-Time Cryptography

Authors: Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan

Abstract: The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory accesses, and thus avoids leaking secrets through cache and timing side-channels. The constant-time property makes a number of implicit assumptions that are fundamentally at odds with the reality of cryptographic code.… ▽ More The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory accesses, and thus avoids leaking secrets through cache and timing side-channels. The constant-time property makes a number of implicit assumptions that are fundamentally at odds with the reality of cryptographic code. Constant-time is not robust. The first issue with constant-time is that it is a whole-program property: It relies on the entirety of the code base being constant-time. But, cryptographic developers do not generally write whole programs; rather, they provide libraries and specific algorithms for other application developers to use. As such, developers of security libraries must maintain their security guarantees even when their code is operating within (potentially untrusted) application contexts. Constant-time requires memory safety. The whole-program nature of constant-time also leads to a second issue: constant-time requires memory safety of all the running code. Any memory safety bugs, whether in the library or the application, will wend their way back to side-channel leaks of secrets if not direct disclosure. And although cryptographic libraries should (and are) written to be memory-safe, it is unfortunately unrealistic to expect the same from every application that uses each library. We formalize robust constant-time and build a RobustIsoCrypt compiler that transforms the library code and protects the secrets even when they are linked with untrusted code. Our evaluation with SUPERCOP benchmarking framework shows that the performance overhead is less than five percent on average. △ Less

Submitted 9 November, 2023; originally announced November 2023.

Semiclassical study of single-molecule magnets and their quantum phase transitions

Authors: David Stefan, Lohr-Robles, Enrique, Lopez-Moreno, Peter Otto Hess

Abstract: We present a study of systems of single-molecule magnets using a semiclassical analysis and catastrophe theory. Separatrices in parameter space are constructed which are useful to determine the structure of the Hamiltonians energy levels. In particular the Maxwell set separatrix determines the behavior of the ground state of the system. We consider an external magnetic field with two components, o… ▽ More We present a study of systems of single-molecule magnets using a semiclassical analysis and catastrophe theory. Separatrices in parameter space are constructed which are useful to determine the structure of the Hamiltonians energy levels. In particular the Maxwell set separatrix determines the behavior of the ground state of the system. We consider an external magnetic field with two components, one parallel to the easy magnetization axis of the molecule and the other perpendicular to it. Using the fidelity and heat capacity we were able to detect the signals of the QPTs as a function of the magnetic field components. △ Less

Submitted 20 June, 2023; originally announced June 2023.

Comments: 11 pages, 7 figures

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

Authors: Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Craig Disselkoen, Aidan Denlinger, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, Deian Stefan

Abstract: Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm -- and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory-Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions… ▽ More Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm -- and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory-Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to precisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler -- and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety) on the PolyBenchC suite. More importantly, MSWasm's design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free. △ Less

Submitted 26 September, 2022; v1 submitted 29 August, 2022; originally announced August 2022.

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back, a Tutorial on Dynamic Information Flow

Authors: Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, Deian Stefan

Abstract: This tutorial provides a complete and homogeneous account of the latest advances in fine- and coarse-grained dynamic information-flow control (IFC) security. Since the 70s, the programming language and the operating system communities have proposed different IFC approaches. IFC operating systems track information flows in a coarse-grained fashion, at the granularity of a process. In contrast, trad… ▽ More This tutorial provides a complete and homogeneous account of the latest advances in fine- and coarse-grained dynamic information-flow control (IFC) security. Since the 70s, the programming language and the operating system communities have proposed different IFC approaches. IFC operating systems track information flows in a coarse-grained fashion, at the granularity of a process. In contrast, traditional language-based approaches to IFC are fine-grained: they track information flows at the granularity of program variables. For decades, researchers believed coarse-grained IFC to be strictly less permissive than fine-grained IFC -- coarse-grained IFC systems seem inherently less precise because they track less information -- and so granularity appeared to be a fundamental feature of IFC systems. We show that the granularity of the tracking system does not fundamentally restrict how precise or permissive dynamic IFC systems can be. To this end, we mechanize two mostly standard languages, one with a fine-grained dynamic IFC system and the other with a coarse-grained dynamic IFC system, and prove a semantics-preserving translation from each language to the other. In addition, we derive the standard security property of non-interference of each language from that of the other via our verified translation. These translations stand to have important implications on the usability of IFC approaches. The coarse- to fine-grained direction can be used to remove the label annotation burden that fine-grained systems impose on developers, while the fine- to coarse-grained translation shows that coarse-grained systems -- which are easier to design and implement -- can track information as precisely as fine-grained systems and provides an algorithm for automatically retrofitting legacy applications to run on existing coarse-grained systems. △ Less

Submitted 29 August, 2022; originally announced August 2022.

A Turning Point for Verified Spectre Sandboxing

Authors: Sunjay Cauligi, Marco Guarnieri, Daniel Moghimi, Deian Stefan, Marco Vassena

Abstract: Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre atta… ▽ More Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to block Spectre attacks, but to date, very few have been formally vetted; most are "best effort" strategies. Formal guarantees are particularly crucial for protecting isolated environments like sandboxing against Spectre attacks. In such environments, a subtle flaw in the mitigation would allow untrusted code to break out of the sandbox and access trusted memory regions. In our work, we develop principled foundations to build isolated environments resistant against Spectre attacks. We propose a formal framework for reasoning about sandbox execution and Spectre attacks. We formalize properties that sound mitigation strategies must fulfill and we show how various existing mitigations satisfy (or fail to satisfy!) these properties. △ Less

Submitted 2 August, 2022; originally announced August 2022.

Separation of track- and shower-like energy deposits in ProtoDUNE-SP using a convolutional neural network

Authors: DUNE Collaboration, A. Abed Abud, B. Abi, R. Acciarri, M. A. Acero, M. R. Adames, G. Adamov, M. Adamowski, D. Adams, M. Adinolfi, A. Aduszkiewicz, J. Aguilar, Z. Ahmad, J. Ahmed, B. Aimard, B. Ali-Mohammadzadeh, T. Alion, K. Allison, S. Alonso Monsalve, M. AlRashed, C. Alt, A. Alton, R. Alvarez, P. Amedo, J. Anderson , et al. (1204 additional authors not shown)

Abstract: Liquid argon time projection chamber detector technology provides high spatial and calorimetric resolutions on the charged particles traversing liquid argon. As a result, the technology has been used in a number of recent neutrino experiments, and is the technology of choice for the Deep Underground Neutrino Experiment (DUNE). In order to perform high precision measurements of neutrinos in the det… ▽ More Liquid argon time projection chamber detector technology provides high spatial and calorimetric resolutions on the charged particles traversing liquid argon. As a result, the technology has been used in a number of recent neutrino experiments, and is the technology of choice for the Deep Underground Neutrino Experiment (DUNE). In order to perform high precision measurements of neutrinos in the detector, final state particles need to be effectively identified, and their energy accurately reconstructed. This article proposes an algorithm based on a convolutional neural network to perform the classification of energy deposits and reconstructed particles as track-like or arising from electromagnetic cascades. Results from testing the algorithm on data from ProtoDUNE-SP, a prototype of the DUNE far detector, are presented. The network identifies track- and shower-like particles, as well as Michel electrons, with high efficiency. The performance of the algorithm is consistent between data and simulation. △ Less

Submitted 30 June, 2022; v1 submitted 31 March, 2022; originally announced March 2022.

Comments: 31 pages, 15 figures

Report number: FERMILAB-PUB-22-240-AD-ESH-LBNF-ND-SCD, CERN-EP-2022-077

Journal ref: Eur.Phys.J.C 82 (2022) 10, 903

Blocked or Broken? Automatically Detecting When Privacy Interventions Break Websites

Authors: Michael Smith, Peter Snyder, Moritz Haller, Benjamin Livshits, Deian Stefan, Hamed Haddadi

Abstract: A core problem in the development and maintenance of crowd-sourced filter lists is that their maintainers cannot confidently predict whether (and where) a new filter list rule will break websites. This is a result of enormity of the Web, which prevents filter list authors from broadly understanding the impact of a new blocking rule before they ship it to millions of users. The inability of filter… ▽ More A core problem in the development and maintenance of crowd-sourced filter lists is that their maintainers cannot confidently predict whether (and where) a new filter list rule will break websites. This is a result of enormity of the Web, which prevents filter list authors from broadly understanding the impact of a new blocking rule before they ship it to millions of users. The inability of filter list authors to evaluate the Web compatibility impact of a new rule before ship** it severely reduces the benefits of filter-list-based content blocking: filter lists are both overly-conservative (i.e. rules are tailored narrowly to reduce the risk of breaking things) and error-prone (i.e. blocking tools still break large numbers of sites). To scale to the size and scope of the Web, filter list authors need an automated system to detect when a new filter rule breaks websites, before that breakage has a chance to make it to end users. In this work, we design and implement the first automated system for predicting when a filter list rule breaks a website. We build a classifier, trained on a dataset generated by a combination of compatibility data from the EasyList project and novel browser instrumentation, and find it is accurate to practical levels (AUC 0.88). Our open source system requires no human interaction when assessing the compatibility risk of a proposed privacy intervention. We also present the 40 page behaviors that most predict breakage in observed websites. △ Less

Submitted 2 May, 2022; v1 submitted 7 March, 2022; originally announced March 2022.

Measurement of the ($π^-$, Ar) total hadronic cross section at the LArIAT experiment

Authors: E. Gramellini, J. Ho, R. Acciarri, C. Adams, J. Asaadi, M. Backfish, W. Badgett, B. Baller, V. Basque, O. Benevides Rodrigues, F. d. M. Blaszczyk, R. Bouabid, C. Bromberg, R. Carey, R. Castillo Fernandez, F. Cavanna, J. I. Cevallos Aleman, A. Chatterjee, P. Dedin, M. V. dos Santos, D. Edmunds, C. Escobar, J. Esquivel, J. J. Evans, A. Falcone , et al. (73 additional authors not shown)

Abstract: We present the first measurement of the negative pion total hadronic cross section on argon, which we performed at the Liquid Argon In A Testbeam (LArIAT) experiment. All hadronic reaction channels, as well as hadronic elastic interactions with scattering angle greater than 5~degrees are included. The pions have a kinetic energies in the range 100-700~MeV and are produced by a beam of charged part… ▽ More We present the first measurement of the negative pion total hadronic cross section on argon, which we performed at the Liquid Argon In A Testbeam (LArIAT) experiment. All hadronic reaction channels, as well as hadronic elastic interactions with scattering angle greater than 5~degrees are included. The pions have a kinetic energies in the range 100-700~MeV and are produced by a beam of charged particles im**ing on a solid target at the Fermilab Test Beam Facility. LArIAT employs a 0.24~ton active mass Liquid Argon Time Projection Chamber (LArTPC) to measure the pion hadronic interactions. For this measurement, LArIAT has developed the ``thin slice method", a new technique to measure cross sections with LArTPCs. While generally higher than the prediction, our measurement of the ($π^-$,Ar) total hadronic cross section is in agreement with the prediction of the Geant4 model when considering a model uncertainty of $\sim$5.1\%. △ Less

Submitted 7 July, 2022; v1 submitted 30 July, 2021; originally announced August 2021.

Comments: 15 pages, 15 figures, 3 tables, accepted by PRD

SoK: Practical Foundations for Software Spectre Defenses

Authors: Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan

Abstract: Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with th… ▽ More Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees. This paper systematizes the community's current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the expressiveness of formal frameworks, the complexity of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses. △ Less

Submitted 8 April, 2022; v1 submitted 12 May, 2021; originally announced May 2021.

Comments: To appear at Oakland '22

Isolation Without Taxation: Near Zero Cost Transitions for SFI

Authors: Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan

Abstract: Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimi… ▽ More Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and companies like Fastly and Cloudflare use SFI to safely co-locate untrusted tenants on their edge clouds. While there have been significant efforts to optimize and verify SFI enforcement, context switching in SFI systems remains largely unexplored: almost all SFI systems use \emph{heavyweight transitions} that are not only error-prone but incur significant performance overhead from saving, clearing, and restoring registers when context switching. We identify a set of \emph{zero-cost conditions} that characterize when sandboxed code has sufficient structured to guarantee security via lightweight \emph{zero-cost} transitions (simple function calls). We modify the Lucet Wasm compiler and its runtime to use zero-cost transitions, eliminating the undue performance tax on systems that rely on Lucet for sandboxing (e.g., we speed up image and font rendering in Firefox by up to 29.7\% and 10\% respectively). To remove the Lucet compiler and its correct implementation of the Wasm specification from the trusted computing base, we (1) develop a \emph{static binary verifier}, VeriZero, which (in seconds) checks that binaries produced by Lucet satisfy our zero-cost conditions, and (2) prove the soundness of VeriZero by develo** a logical relation that captures when a compiled Wasm function is semantically well-behaved with respect to our zero-cost conditions. Finally, we show that our model is useful beyond Wasm by describing a new, purpose-built SFI system, SegmentZero32, that uses x86 segmentation and LLVM with mostly off-the-shelf passes to enforce our zero-cost conditions; our prototype performs on-par with the state-of-the-art Native Client SFI system. △ Less

Submitted 18 November, 2021; v1 submitted 30 April, 2021; originally announced May 2021.

Solver-Aided Constant-Time Circuit Verification

Authors: Rami Gokhan Kici, Klaus v. Gleissenthall, Deian Stefan, Ranjit Jhala

Abstract: We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exp… ▽ More We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verification failures via a new notion of constant-time counterexamples, which Xenon uses to automatically synthesize a minimal set of secrecy assumptions. Xenon further exploits modularity in Verilog code via a notion of module summaries, thereby avoiding duplicate work across multiple module instantiations. We show how Xenon's assumption synthesis and summaries enable the verification of a variety of circuits including AES, a highly modular AES-256 implementation where modularity cuts verification from six hours to under three seconds, and ScarV, a timing channel hardened RISC-V micro-controller whose size exceeds previously verified designs by an order of magnitude. △ Less

Submitted 1 April, 2021; originally announced April 2021.

Swivel: Hardening WebAssembly against Spectre

Authors: Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, Deian Stefan

Abstract: We describe Swivel, a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Outside the browser, Wasm has become a popular lightweight, in-process sandbox and is, for example, used in production to isolate different clients on edge clouds and function-as-a-service platforms. Unfortunately, Spectre attacks can bypass Wasm's isolation guarantees. Swivel hardens Wasm agains… ▽ More We describe Swivel, a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Outside the browser, Wasm has become a popular lightweight, in-process sandbox and is, for example, used in production to isolate different clients on edge clouds and function-as-a-service platforms. Unfortunately, Spectre attacks can bypass Wasm's isolation guarantees. Swivel hardens Wasm against this class of attacks by ensuring that potentially malicious code can neither use Spectre attacks to break out of the Wasm sandbox nor coerce victim code-another Wasm client or the embedding process-to leak secret data. We describe two Swivel designs, a software-only approach that can be used on existing CPUs, and a hardware-assisted approach that uses extension available in Intel 11th generation CPUs. For both, we evaluate a randomized approach that mitigates Spectre and a deterministic approach that eliminates Spectre altogether. Our randomized implementations impose under 10.3% overhead on the Wasm-compatible subset of SPEC 2006, while our deterministic implementations impose overheads between 3.3% and 240.2%. Though high on some benchmarks, Swivel's overhead is still between 9x and 36.3x smaller than existing defenses that rely on pipeline fences. △ Less

Submitted 19 March, 2021; v1 submitted 25 February, 2021; originally announced February 2021.

Comments: Accepted at USENIX 21

MSC Class: D.4.6 ACM Class: D.4.6

Study of scintillation light collection, production and propagation in a 4 tonne dual-phase LArTPC

Authors: B. Aimard, L. Aizawa, C. Alt, J. Asaadi, M. Auger, V. Aushev, D. Autiero, A. Balaceanu, G. Balik, L. Balleyguier, E. Bechetoille, D. Belver, A. M. Blebea-Apostu, S. Bolognesi, S. Bordoni, N. Bourgeois, B. Bourguille, J. Bremer, G. Brown, G. Brunetti, L. Brunetti, D. Caiulo, M. Calin, E. Calvo, M. Campanelli , et al. (138 additional authors not shown)

Abstract: The $3 \times 1 \times 1$ m$^3$ demonstrator is a dual phase liquid argon time projection chamber that has recorded cosmic rays events in 2017 at CERN. The light signal in these detectors is crucial to provide precise timing capabilities. The performances of the photon detection system, composed of five PMTs, are discussed. The collected scintillation and electroluminescence light created by passi… ▽ More The $3 \times 1 \times 1$ m$^3$ demonstrator is a dual phase liquid argon time projection chamber that has recorded cosmic rays events in 2017 at CERN. The light signal in these detectors is crucial to provide precise timing capabilities. The performances of the photon detection system, composed of five PMTs, are discussed. The collected scintillation and electroluminescence light created by passing particles has been studied in various detector conditions. In particular, the scintillation light production and propagation processes have been analyzed and compared to simulations, improving the understanding of some liquid argon properties. △ Less

Submitted 20 December, 2020; v1 submitted 16 October, 2020; originally announced October 2020.

Comments: 30 pages, 26 figures

First results on ProtoDUNE-SP liquid argon time projection chamber performance from a beam test at the CERN Neutrino Platform

Authors: DUNE Collaboration, B. Abi, A. Abed Abud, R. Acciarri, M. A. Acero, G. Adamov, M. Adamowski, D. Adams, P. Adrien, M. Adinolfi, Z. Ahmad, J. Ahmed, T. Alion, S. Alonso Monsalve, C. Alt, J. Anderson, C. Andreopoulos, M. P. Andrews, F. Andrianala, S. Andringa, A. Ankowski, M. Antonova, S. Antusch, A. Aranda-Fernandez, A. Ariga , et al. (970 additional authors not shown)

Abstract: The ProtoDUNE-SP detector is a single-phase liquid argon time projection chamber with an active volume of $7.2\times 6.0\times 6.9$ m$^3$. It is installed at the CERN Neutrino Platform in a specially-constructed beam that delivers charged pions, kaons, protons, muons and electrons with momenta in the range 0.3 GeV$/c$ to 7 GeV/$c$. Beam line instrumentation provides accurate momentum measurements… ▽ More The ProtoDUNE-SP detector is a single-phase liquid argon time projection chamber with an active volume of $7.2\times 6.0\times 6.9$ m$^3$. It is installed at the CERN Neutrino Platform in a specially-constructed beam that delivers charged pions, kaons, protons, muons and electrons with momenta in the range 0.3 GeV$/c$ to 7 GeV/$c$. Beam line instrumentation provides accurate momentum measurements and particle identification. The ProtoDUNE-SP detector is a prototype for the first far detector module of the Deep Underground Neutrino Experiment, and it incorporates full-size components as designed for that module. This paper describes the beam line, the time projection chamber, the photon detectors, the cosmic-ray tagger, the signal processing and particle reconstruction. It presents the first results on ProtoDUNE-SP's performance, including noise and gain measurements, $dE/dx$ calibration for muons, protons, pions and electrons, drift electron lifetime measurements, and photon detector noise, signal sensitivity and time resolution measurements. The measured values meet or exceed the specifications for the DUNE far detector, in several cases by large margins. ProtoDUNE-SP's successful operation starting in 2018 and its production of large samples of high-quality data demonstrate the effectiveness of the single-phase far detector design. △ Less

Submitted 3 June, 2021; v1 submitted 13 July, 2020; originally announced July 2020.

Comments: 93 pages, 70 figures

Report number: FERMILAB-PUB-20-059-AD-ESH-LBNF-ND-SCD, CERN-EP-2020-125

Journal ref: JINST 15 (2020) P12004

Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade

Authors: Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean Tullsen, Deian Stefan

Abstract: We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via speculation, it suffices to $\textit{cut}$ the dataflow from expressions that speculatively introduce secrets ($\textit{sources}$) to those that leak them through the cache ($\textit{sinks}$), rather than prohibit speculation… ▽ More We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via speculation, it suffices to $\textit{cut}$ the dataflow from expressions that speculatively introduce secrets ($\textit{sources}$) to those that leak them through the cache ($\textit{sinks}$), rather than prohibit speculation altogether. We formalize this insight in a $\textit{static type system}$ that (1) types each expression as either $\textit{transient}$, i.e., possibly containing speculative secrets or as being $\textit{stable}$, and (2) prohibits speculative leaks by requiring that all $\textit{sink}$ expressions are stable. BLADE relies on a new new abstract primitive, $\textbf{protect}$, to halt speculation at fine granularity. We formalize and implement $\textbf{protect}$ using existing architectural mechanisms, and show how BLADE's type system can automatically synthesize a $\textit{minimal}$ number of $\textbf{protect}$s to provably eliminate speculative leaks. We implement BLADE in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation $\textit{automatically}$, without user intervention, and $\textit{efficiently}$ even when using fences to implement $\textbf{protect}$. △ Less

Submitted 7 December, 2020; v1 submitted 1 May, 2020; originally announced May 2020.

Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version)

Authors: Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, Deian Stefan

Abstract: Firefox and other major browsers rely on dozens of third-party libraries to render audio, video, images, and other content. These libraries are a frequent source of vulnerabilities. To mitigate this threat, we are migrating Firefox to an architecture that isolates these libraries in lightweight sandboxes, dramatically reducing the impact of a compromise. Retrofitting isolation can be labor-inten… ▽ More Firefox and other major browsers rely on dozens of third-party libraries to render audio, video, images, and other content. These libraries are a frequent source of vulnerabilities. To mitigate this threat, we are migrating Firefox to an architecture that isolates these libraries in lightweight sandboxes, dramatically reducing the impact of a compromise. Retrofitting isolation can be labor-intensive, very prone to security bugs, and requires critical attention to performance. To help, we developed RLBox, a framework that minimizes the burden of converting Firefox to securely and efficiently use untrusted code. To enable this, RLBox employs static information flow enforcement, and lightweight dynamic checks, expressed directly in the C++ type system. RLBox supports efficient sandboxing through either software-based-fault isolation or multi-core process isolation. Performance overheads are modest and transient, and have only minor impact on page latency. We demonstrate this by sandboxing performance-sensitive image decoding libraries ( libjpeg and libpng ), video decoding libraries ( libtheora and libvpx ), the libvorbis audio decoding library, and the zlib decompression library. RLBox, using a WebAssembly sandbox, has been integrated into production Firefox to sandbox the libGraphite font sha** library. △ Less

Submitted 9 March, 2020; v1 submitted 1 March, 2020; originally announced March 2020.

Comments: Accepted at Usenix Security 2020

MSC Class: D.4.6 ACM Class: D.4.6

Design and performance of a 35-ton liquid argon time projection chamber as a prototype for future very large detectors

Authors: D. L. Adams, M. Baird, G. Barr, N. Barros, A. Blake, E. Blaufuss, A. Booth, D. Brailsford, N. Buchanan, B. Carls, H. Chen, M. Convery, G. De Geronimo, T. Dealtry, R. Dharmapalan, Z. Djurcic, J. Fowler, S. Glavin, R. A. Gomes, M. C. Goodman, M. Graham, L. Greenler, A. Hahn, J. Hartnell, R. Herbst , et al. (49 additional authors not shown)

Abstract: Liquid argon time projection chamber technology is an attractive choice for large neutrino detectors, as it provides a high-resolution active target and it is expected to be scalable to very large masses. Consequently, it has been chosen as the technology for the first module of the DUNE far detector. However, the fiducial mass required for "far detectors" of the next generation of neutrino oscill… ▽ More Liquid argon time projection chamber technology is an attractive choice for large neutrino detectors, as it provides a high-resolution active target and it is expected to be scalable to very large masses. Consequently, it has been chosen as the technology for the first module of the DUNE far detector. However, the fiducial mass required for "far detectors" of the next generation of neutrino oscillation experiments far exceeds what has been demonstrated so far. Scaling to this larger mass, as well as the requirement for underground construction places a number of additional constraints on the design. A prototype 35-ton cryostat was built at Fermi National Acccelerator Laboratory to test the functionality of the components foreseen to be used in a very large far detector. The Phase I run, completed in early 2014, demonstrated that liquid argon could be maintained at sufficient purity in a membrane cryostat. A time projection chamber was installed for the Phase II run, which collected data in February and March of 2016. The Phase II run was a test of the modular anode plane assemblies with wrapped wires, cold readout electronics, and integrated photon detection systems. While the details of the design do not match exactly those chosen for the DUNE far detector, the 35-ton TPC prototype is a demonstration of the functionality of the basic components. Measurements are performed using the Phase II data to extract signal and noise characteristics and to align the detector components. A measurement of the electron lifetime is presented, and a novel technique for measuring a track's position based on pulse properties is described. △ Less

Submitted 2 March, 2020; v1 submitted 18 December, 2019; originally announced December 2019.

Comments: 28 pages, 12 figures, accepted by JINST

Gobi: WebAssembly as a Practical Path to Library Sandboxing

Authors: Shravan Narayan, Tal Garfinkel, Sorin Lerner, Hovav Shacham, Deian Stefan

Abstract: Software based fault isolation (SFI) is a powerful approach to reduce the impact of security vulnerabilities in large C/C++ applications like Firefox and Apache. Unfortunately, practical SFI tools have not been broadly available. Develo** SFI toolchains are a significant engineering challenge. Only in recent years have browser vendors invested in building production quality SFI tools like Nati… ▽ More Software based fault isolation (SFI) is a powerful approach to reduce the impact of security vulnerabilities in large C/C++ applications like Firefox and Apache. Unfortunately, practical SFI tools have not been broadly available. Develo** SFI toolchains are a significant engineering challenge. Only in recent years have browser vendors invested in building production quality SFI tools like Native Client (NaCl) to sandbox code. Further, without committed support, these tools are not viable, e.g. NaCl has been discontinued, orphaning projects that relied on it. WebAssembly (Wasm) offers a promising solution---it can support high performance sandboxing and has been embraced by all major browser vendors---thus seems to have a viable future. However, Wasm presently only offers a solution for sandboxing mobile code. Providing SFI for native application, such as C/C++ libraries requires additional steps. To reconcile the different worlds of Wasm on the browser and native platforms, we present Gobi. Gobi is a system of compiler changes and runtime support that can sandbox normal C/C++ libraries with Wasm---allowing them to be compiled and linked into native applications. Gobi has been tested on libjpeg, libpng, and zlib. Based on our experience develo** Gobi, we conclude with a call to arms to the Wasm community and SFI research community to make Wasm based module sandboxing a first class use case and describe how this can significantly benefit both communities. Addendum: This short paper was originally written in January of 2019. Since then, the implementation and design of Gobi has evolved substantially as some of the issues raised in this paper have been addressed by the Wasm community. Nevertheless, several challenges still remain. We have thus left the paper largely intact and only provide a brief update on the state of Wasm tooling as of November 2019 in the last section. △ Less

Submitted 4 December, 2019; originally announced December 2019.

MSC Class: D.4.6 ACM Class: D.4.6

The Liquid Argon In A Testbeam (LArIAT) Experiment

Authors: LArIAT Collaboration, R. Acciarri, C. J. Adams, J. Asaadi, M. Backfish, W. Badgett, B. Baller, O. Benevides Rodrigues, F. d. M. Blaszczyk, R. Bouabid, C. Bromberg, R. Carey, R. Castillo Fernandez, F. Cavanna, J. I. Cevallos Aleman, A. Chatterjee, P. Dedin Neto, M. V. Dos Santos, S. Dytman, D. Edmunds, M. Elkins, C. O. Escobar, J. Esquivel, J. Evans, A. Falcone , et al. (81 additional authors not shown)

Abstract: The LArIAT liquid argon time projection chamber, placed in a tertiary beam of charged particles at the Fermilab Test Beam Facility, has collected large samples of pions, muons, electrons, protons, and kaons in the momentum range 300-1400 MeV/c. This paper describes the main aspects of the detector and beamline, and also reports on calibrations performed for the detector and beamline components. The LArIAT liquid argon time projection chamber, placed in a tertiary beam of charged particles at the Fermilab Test Beam Facility, has collected large samples of pions, muons, electrons, protons, and kaons in the momentum range 300-1400 MeV/c. This paper describes the main aspects of the detector and beamline, and also reports on calibrations performed for the detector and beamline components. △ Less

Submitted 6 February, 2020; v1 submitted 23 November, 2019; originally announced November 2019.

Report number: FERMILAB-PUB-19-460-ND

Iodine: Verifying Constant-Time Execution of Hardware

Authors: Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, Ranjit Jhala

Abstract: To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing channels are ubiquitous in modern hardware, due to its labyrinthine fast-paths and optimizations. A promising way to avoid timing vulnerabilities is to devise --- and verify --- conditions under which a hardware design is… ▽ More To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing channels are ubiquitous in modern hardware, due to its labyrinthine fast-paths and optimizations. A promising way to avoid timing vulnerabilities is to devise --- and verify --- conditions under which a hardware design is free of timing variability, i.e., executes in constant-time. In this paper, we present Iodine: a clock precise, constant-time approach to eliminating timing side channels in hardware. Iodine succeeds in verifying various open source hardware designs in seconds and with little developer effort. Iodine also discovered two constant-time violations: one in a floating-point unit and another one in an RSA encryption module. △ Less

Submitted 7 October, 2019; originally announced October 2019.

Journal ref: USENIX Security Symposium 2019: 1411-1428

Constant-Time Foundations for the New Spectre Era

Authors: Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe

Abstract: The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time a… ▽ More The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful. This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries. △ Less

Submitted 8 May, 2020; v1 submitted 3 October, 2019; originally announced October 2019.

Comments: To appear at PLDI '20

CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem

Authors: Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, Deian Stefan

Abstract: A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ecosystem" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the new introduction of the WebAssembly byt… ▽ More A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to match the convenience that comes from its ubiquitous support on the "web ecosystem" - the wide variety of technologies that collectively underpins the modern World Wide Web. With the new introduction of the WebAssembly bytecode language (Wasm) into the web ecosystem, we have a unique opportunity to advance a principled alternative to existing JavaScript cryptography use cases which does not compromise this convenience. We present Constant-Time WebAssembly (CT-Wasm), a type-driven strict extension to WebAssembly which facilitates the verifiably secure implementation of cryptographic algorithms. CT-Wasm's type system ensures that code written in CT-Wasm is both information flow secure and resistant to timing side channel attacks; like base Wasm, these guarantees are verifiable in linear time. Building on an existing Wasm mechanization, we mechanize the full CT-Wasm specification, prove soundness of the extended type system, implement a verified type checker, and give several proofs of the language's security properties. We provide two implementations of CT-Wasm: an OCaml reference interpreter and a native implementation for Node.js and Chromium that extends Google's V8 engine. We also implement a CT-Wasm to Wasm rewrite tool that allows developers to reap the benefits of CT-Wasm's type system today, while develo** cryptographic algorithms for base Wasm environments. We evaluate the language, our implementations, and supporting tools by porting several cryptographic primitives - Salsa20, SHA-256, and TEA - and the full TweetNaCl library. We find that CT-Wasm is fast, expressive, and generates code that we experimentally measure to be constant-time. △ Less

Submitted 17 December, 2018; v1 submitted 3 August, 2018; originally announced August 2018.

Comments: 29 pages, 9 figures

A 4 tonne demonstrator for large-scale dual-phase liquid argon time projection chambers

Authors: B. Aimard, Ch. Alt, J. Asaadi, M. Auger, V. Aushev, D. Autiero, M. M. Badoi, A. Balaceanu, G. Balik, L. Balleyguier, E. Bechetoille, D. Belver, A. M. Blebea-Apostu, S. Bolognesi, S. Bordoni, N. Bourgeois, B. Bourguille, J. Bremer, G. Brown, G. Brunetti, L. Brunetti, D. Caiulo, M. Calin, E. Calvo, M. Campanelli , et al. (147 additional authors not shown)

Abstract: A 10 kilo-tonne dual-phase liquid argon TPC is one of the detector options considered for the Deep Underground Neutrino Experiment (DUNE). The detector technology relies on amplification of the ionisation charge in ultra-pure argon vapour and oers several advantages compared to the traditional single-phase liquid argon TPCs. A 4.2 tonne dual-phase liquid argon TPC prototype, the largest of its kin… ▽ More A 10 kilo-tonne dual-phase liquid argon TPC is one of the detector options considered for the Deep Underground Neutrino Experiment (DUNE). The detector technology relies on amplification of the ionisation charge in ultra-pure argon vapour and oers several advantages compared to the traditional single-phase liquid argon TPCs. A 4.2 tonne dual-phase liquid argon TPC prototype, the largest of its kind, with an active volume of 3x1x1 $m^3$ has been constructed and operated at CERN. In this paper we describe in detail the experimental setup and detector components as well as report on the operation experience. We also present the first results on the achieved charge amplification, prompt scintillation and electroluminescence detection, and purity of the liquid argon from analyses of a collected sample of cosmic ray muons. △ Less

Submitted 19 October, 2018; v1 submitted 8 June, 2018; originally announced June 2018.

Photon detector system timing performance in the DUNE 35-ton prototype liquid argon time projection chamber

Authors: D. L. Adams, T. Alion, J. T. Anderson, L. Bagby, M. Baird, G. Barr, N. Barros, K. Biery, A. Blake, E. Blaufuss, T. Boone, A. Booth, D. Brailsford, N. Buchanan, A. Chatterjee, M. Convery, J. Davies, T. Dealtry, P. DeLurgio, G. Deuerling, R. Dharmapalan, Z. Djurcic, G. Drake, B. Eberly, J. Freeman , et al. (53 additional authors not shown)

Abstract: The 35-ton prototype for the Deep Underground Neutrino Experiment far detector was a single-phase liquid argon time projection chamber with an integrated photon detector system, all situated inside a membrane cryostat. The detector took cosmic-ray data for six weeks during the period of February 1, 2016 to March 12, 2016. The performance of the photon detection system was checked with these data.… ▽ More The 35-ton prototype for the Deep Underground Neutrino Experiment far detector was a single-phase liquid argon time projection chamber with an integrated photon detector system, all situated inside a membrane cryostat. The detector took cosmic-ray data for six weeks during the period of February 1, 2016 to March 12, 2016. The performance of the photon detection system was checked with these data. An installed photon detector was demonstrated to measure the arrival times of cosmic-ray muons with a resolution better than 32 ns, limited by the timing of the trigger system. A measurement of the timing resolution using closely-spaced calibration pulses yielded a resolution of 15 ns for pulses at a level of 6 photo-electrons. Scintillation light from cosmic-ray muons was observed to be attenuated with increasing distance with a characteristic length of $155 \pm 28$ cm. △ Less

Submitted 5 June, 2018; v1 submitted 16 March, 2018; originally announced March 2018.

Comments: 17 pages, 8 figures. Submitted to JINST

$PBW$-deformations of graded rings

Authors: Alessandro Ardizzoni, Paolo Saracco, Dragoş Ştefan

Abstract: We prove in a very general framework several versions of the classical Poincaré-Birkhoff-Witt Theorem, which extend results from [BeGi, BrGa, CS, HvOZ, WW]. Applications and examples are discussed in the last part of the paper. We prove in a very general framework several versions of the classical Poincaré-Birkhoff-Witt Theorem, which extend results from [BeGi, BrGa, CS, HvOZ, WW]. Applications and examples are discussed in the last part of the paper. △ Less

Submitted 12 October, 2017; originally announced October 2017.

MSC Class: 17C25 (Primary); 16W50; 16E40 (Secondary)

Journal ref: Israel J. Math. 249 (2022), no. 2, 769-856

The Single-Phase ProtoDUNE Technical Design Report

Authors: B. Abi, R. Acciarri, M. A. Acero, M. Adamowski, C. Adams, D. L. Adams, P. Adamson, M. Adinolfi, Z. Ahmad, C. H. Albright, T. Alion, J. Anderson, K. Anderson, C. Andreopoulos, M. P. Andrews, R. A. Andrews, J. dos Anjos, A. Ankowski, J. Anthony, M. Antonello, A. Aranda Fernandez, A. Ariga, T. Ariga, E. Arrieta Diaz, J. Asaadi , et al. (806 additional authors not shown)

Abstract: ProtoDUNE-SP is the single-phase DUNE Far Detector prototype that is under construction and will be operated at the CERN Neutrino Platform (NP) starting in 2018. ProtoDUNE-SP, a crucial part of the DUNE effort towards the construction of the first DUNE 10-kt fiducial mass far detector module (17 kt total LAr mass), is a significant experiment in its own right. With a total liquid argon (LAr) mass… ▽ More ProtoDUNE-SP is the single-phase DUNE Far Detector prototype that is under construction and will be operated at the CERN Neutrino Platform (NP) starting in 2018. ProtoDUNE-SP, a crucial part of the DUNE effort towards the construction of the first DUNE 10-kt fiducial mass far detector module (17 kt total LAr mass), is a significant experiment in its own right. With a total liquid argon (LAr) mass of 0.77 kt, it represents the largest monolithic single-phase LArTPC detector to be built to date. It's technical design is given in this report. △ Less

Submitted 27 July, 2017; v1 submitted 21 June, 2017; originally announced June 2017.

Comments: 165 pages, fix references, author list and minor numbers

Muon momentum measurement in ICARUS-T600 LAr-TPC via multiple scattering in few-GeV range

Authors: Maddalena Antonello, Bagdat Baibussinov, Vincenzo Bellini, Pietro Angelo Benetti, Fabrizio Boffelli, Arkadiusz Bubak, Elio Calligarich, Sandro Centro, Tommaso Cervi, Alessandra Cesana, Krzysztof Cieslik, Alfredo G. Cocco, Anna Dabrowska, Alexander Dermenev, Andrea Falcone, Christian Farnese, Angela Fava, Alfredo Ferrari, Daniele Gibin, Sergei Gninenko, Alberto Guglielmi, Malgorzata Haranczyk, Jacek Holeczek, Michal Janik, Mikhail Kirsanov , et al. (32 additional authors not shown)

Abstract: The measurement of muon momentum by Multiple Coulomb Scattering is a crucial ingredient to the reconstruction of νμ CC events in the ICARUS-T600 liquid argon TPC in absence of magnetic field, as in the search for sterile neutrinos at Fermilab where ICARUS will be exposed to ~1 GeV Booster neutrino beam. A sample of ~1000 stop** muons produced by charged current interactions of CNGS νμ in the sur… ▽ More The measurement of muon momentum by Multiple Coulomb Scattering is a crucial ingredient to the reconstruction of νμ CC events in the ICARUS-T600 liquid argon TPC in absence of magnetic field, as in the search for sterile neutrinos at Fermilab where ICARUS will be exposed to ~1 GeV Booster neutrino beam. A sample of ~1000 stop** muons produced by charged current interactions of CNGS νμ in the surrounding rock at the INFN Gran Sasso underground Laboratory provides an ideal benchmark in the few-GeV range since their momentum can be directly and independently obtained by the calorimetric measurement. Stop** muon momentum in the 0.5- 4.5 GeV/c range has been reconstructed via Multiple Coulomb Scattering with resolution ranging from 10 to 25 % depending on muon energy, track length and uniformity of the electric field in the drift volume. △ Less

Submitted 28 February, 2017; v1 submitted 22 December, 2016; originally announced December 2016.

Comments: 20 pages, 20 figures

Liquid Information Flow Control

Authors: Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama

Abstract: We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, the… ▽ More We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application. The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time. △ Less

Submitted 30 June, 2020; v1 submitted 12 July, 2016; originally announced July 2016.

On Koszulity of Finite Posets

Authors: Adrian Manea, Dragoş Ştefan

Abstract: We prove in a unifying way several equivalent descriptions of Koszul rings, some of which being well known in the literature. Most of them are stated in terms of coring theoretical properties of $\Tor_n^A(R,R)$. As an application of these characterizations we investigate the Koszulity of the incidence rings for finite graded posets. Based on these results, we describe an algorithm to produce new c… ▽ More We prove in a unifying way several equivalent descriptions of Koszul rings, some of which being well known in the literature. Most of them are stated in terms of coring theoretical properties of $\Tor_n^A(R,R)$. As an application of these characterizations we investigate the Koszulity of the incidence rings for finite graded posets. Based on these results, we describe an algorithm to produce new classes of Koszul posets (i.e. graded posets whose incidence rings are Koszul). Specific examples of Koszul posets are included. △ Less

Submitted 18 May, 2016; originally announced May 2016.

Comments: 14 pages; 4 figures. The first version of arXiv:1504.03548 was split into two parts, the present article containing one of them

MSC Class: Primary 16E40; Secondary 16T15

Long-Baseline Neutrino Facility (LBNF) and Deep Underground Neutrino Experiment (DUNE) Conceptual Design Report Volume 1: The LBNF and DUNE Projects

Authors: R. Acciarri, M. A. Acero, M. Adamowski, C. Adams, P. Adamson, S. Adhikari, Z. Ahmad, C. H. Albright, T. Alion, E. Amador, J. Anderson, K. Anderson, C. Andreopoulos, M. Andrews, R. Andrews, I. Anghel, J. d. Anjos, A. Ankowski, M. Antonello, A. ArandaFernandez, A. Ariga, T. Ariga, D. Aristizabal, E. Arrieta-Diaz, K. Aryal , et al. (780 additional authors not shown)

Abstract: This document presents the Conceptual Design Report (CDR) put forward by an international neutrino community to pursue the Deep Underground Neutrino Experiment at the Long-Baseline Neutrino Facility (LBNF/DUNE), a groundbreaking science experiment for long-baseline neutrino oscillation studies and for neutrino astrophysics and nucleon decay searches. The DUNE far detector will be a very large modu… ▽ More This document presents the Conceptual Design Report (CDR) put forward by an international neutrino community to pursue the Deep Underground Neutrino Experiment at the Long-Baseline Neutrino Facility (LBNF/DUNE), a groundbreaking science experiment for long-baseline neutrino oscillation studies and for neutrino astrophysics and nucleon decay searches. The DUNE far detector will be a very large modular liquid argon time-projection chamber (LArTPC) located deep underground, coupled to the LBNF multi-megawatt wide-band neutrino beam. DUNE will also have a high-resolution and high-precision near detector. △ Less

Submitted 20 January, 2016; originally announced January 2016.

Long-Baseline Neutrino Facility (LBNF) and Deep Underground Neutrino Experiment (DUNE) Conceptual Design Report, Volume 4 The DUNE Detectors at LBNF

Authors: R. Acciarri, M. A. Acero, M. Adamowski, C. Adams, P. Adamson, S. Adhikari, Z. Ahmad, C. H. Albright, T. Alion, E. Amador, J. Anderson, K. Anderson, C. Andreopoulos, M. Andrews, R. Andrews, I. Anghel, J. d. Anjos, A. Ankowski, M. Antonello, A. ArandaFernandez, A. Ariga, T. Ariga, D. Aristizabal, E. Arrieta-Diaz, K. Aryal , et al. (779 additional authors not shown)

Abstract: A description of the proposed detector(s) for DUNE at LBNF A description of the proposed detector(s) for DUNE at LBNF △ Less

Submitted 12 January, 2016; originally announced January 2016.

Long-Baseline Neutrino Facility (LBNF) and Deep Underground Neutrino Experiment (DUNE) Conceptual Design Report Volume 2: The Physics Program for DUNE at LBNF

Authors: DUNE Collaboration, R. Acciarri, M. A. Acero, M. Adamowski, C. Adams, P. Adamson, S. Adhikari, Z. Ahmad, C. H. Albright, T. Alion, E. Amador, J. Anderson, K. Anderson, C. Andreopoulos, M. Andrews, R. Andrews, I. Anghel, J. d. Anjos, A. Ankowski, M. Antonello, A. ArandaFernandez, A. Ariga, T. Ariga, D. Aristizabal, E. Arrieta-Diaz , et al. (780 additional authors not shown)

Abstract: The Physics Program for the Deep Underground Neutrino Experiment (DUNE) at the Fermilab Long-Baseline Neutrino Facility (LBNF) is described. The Physics Program for the Deep Underground Neutrino Experiment (DUNE) at the Fermilab Long-Baseline Neutrino Facility (LBNF) is described. △ Less

Submitted 22 January, 2016; v1 submitted 18 December, 2015; originally announced December 2015.

On Dynamic Flow-Sensitive Floating-Label Systems

Authors: Pablo Buiras, Deian Stefan, Alejandro Russo

Abstract: Flow-sensitive analysis for information-flow control (IFC) allows data structures to have mutable security labels, i.e., labels that can change over the course of the computation. This feature is often used to boost the permissiveness of the IFC monitor, by rejecting fewer runs of programs, and to reduce the burden of explicit label annotations. However, adding flow-sensitive constructs (e.g., ref… ▽ More Flow-sensitive analysis for information-flow control (IFC) allows data structures to have mutable security labels, i.e., labels that can change over the course of the computation. This feature is often used to boost the permissiveness of the IFC monitor, by rejecting fewer runs of programs, and to reduce the burden of explicit label annotations. However, adding flow-sensitive constructs (e.g., references or files) to a dynamic IFC system is subtle and may also introduce high-bandwidth covert channels. In this work, we extend LIO---a language-based floating-label system---with flow-sensitive references. The key insight to safely manipulating the label of a reference is to not only consider the label on the data stored in the reference, i.e., the reference label, but also the label on the reference label itself. Taking this into consideration, we provide an upgrade primitive that can be used to change the label of a reference in a safe manner. We additionally provide a mechanism for automatic upgrades to eliminate the burden of determining when a reference should be upgraded. This approach naturally extends to a concurrent setting, which has not been previously considered by dynamic flow-sensitive systems. For both our sequential and concurrent calculi we prove non-interference by embedding the flow-sensitive system into the original, flow-insensitive LIO calculus---a surprising result on its own. △ Less

Submitted 22 July, 2015; originally announced July 2015.

Electron Neutrino Classification in Liquid Argon Time Projection Chamber Detector

Authors: Piotr Płoński, Dorota Stefan, Robert Sulej, Krzysztof Zaremba

Abstract: Neutrinos are one of the least known elementary particles. The detection of neutrinos is an extremely difficult task since they are affected only by weak sub-atomic force or gravity. Therefore large detectors are constructed to reveal neutrino's properties. Among them the Liquid Argon Time Projection Chamber (LAr-TPC) detectors provide excellent imaging and particle identification ability for stud… ▽ More Neutrinos are one of the least known elementary particles. The detection of neutrinos is an extremely difficult task since they are affected only by weak sub-atomic force or gravity. Therefore large detectors are constructed to reveal neutrino's properties. Among them the Liquid Argon Time Projection Chamber (LAr-TPC) detectors provide excellent imaging and particle identification ability for studying neutrinos. The computerized methods for automatic reconstruction and identification of particles are needed to fully exploit the potential of the LAr-TPC technique. Herein, the novel method for electron neutrino classification is presented. The method constructs a feature descriptor from images of observed event. It characterizes the signal distribution propagated from vertex of interest, where the particle interacts with the detector medium. The classifier is learned with a constructed feature descriptor to decide whether the images represent the electron neutrino or cascade produced by photons. The proposed approach assumes that the position of primary interaction vertex is known. The method's performance in dependency to the noise in a primary vertex position and deposited energy of particles is studied. △ Less

Submitted 3 May, 2015; originally announced May 2015.

Comments: 9 pages

Further Properties and Applications of Koszul Pairs

Authors: Adrian Manea, Dragoş Ştefan

Abstract: Koszul pairs were introduced in [arXiv:1011.4243] as an instrument for the study of Koszul rings. In this paper, we continue the enquiry of such pairs, focusing on the description of the second component, as a follow-up of the study in [arXiv:1605.05458]. As such, we introduce Koszul corings and prove several equivalent characterizations for them. As applications, in the case of locally finite… ▽ More Koszul pairs were introduced in [arXiv:1011.4243] as an instrument for the study of Koszul rings. In this paper, we continue the enquiry of such pairs, focusing on the description of the second component, as a follow-up of the study in [arXiv:1605.05458]. As such, we introduce Koszul corings and prove several equivalent characterizations for them. As applications, in the case of locally finite $R$-rings, we show that a graded $R$-ring is Koszul if and only if its left (or right) graded dual coring is Koszul. Finally, for finite graded posets, we obtain that the respective incidence ring is Koszul if and only if the incidence coring is so. △ Less

Submitted 14 September, 2016; v1 submitted 14 April, 2015; originally announced April 2015.

Comments: part of the first version

MSC Class: 16E40; 16T10; 16T15

Journal ref: SIGMA 12 (2016), 092, 24 pages

Operation and performance of the ICARUS-T600 cryogenic plant at Gran Sasso underground Laboratory

Authors: M. Antonello, P. Aprili, B. Baibussinov, F. Boffelli, A. Bubak, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieślik, D. B. Cline, A. G. Cocco, A. Dabrowski, A. Dermenev, J. M. Disdier, A. Falcone, C. Farnese, A. Fava, A. Ferrari, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, A. Ivashkin , et al. (33 additional authors not shown)

Abstract: ICARUS T600 liquid argon time projection chamber is the first large mass electronic detector of a new generation able to combine the imaging capabilities of the old bubble chambers with the excellent calorimetric energy measurement. After the three months demonstration run on surface in Pavia during 2001, the T600 cryogenic plant was significantly revised, in terms of reliability and safety, in vi… ▽ More ICARUS T600 liquid argon time projection chamber is the first large mass electronic detector of a new generation able to combine the imaging capabilities of the old bubble chambers with the excellent calorimetric energy measurement. After the three months demonstration run on surface in Pavia during 2001, the T600 cryogenic plant was significantly revised, in terms of reliability and safety, in view of its long-term operation in an underground environment. The T600 detector was activated in Hall B of the INFN Gran Sasso Laboratory during Spring 2010, where it was operated without interruption for about three years, taking data exposed to the CERN to Gran Sasso long baseline neutrino beam and cosmic rays. In this paper the T600 cryogenic plant is described in detail together with the commissioning procedures that lead to the successful operation of the detector shortly after the end of the filling with liquid Argon. Overall plant performance and stability during the long-term underground operation are discussed. Finally, the decommissioning procedures, carried out about six months after the end of the CNGS neutrino beam operation, are reported. △ Less

Submitted 22 April, 2015; v1 submitted 7 April, 2015; originally announced April 2015.

Comments: 27 pages; corrected typos; added references and reshuffled reference list (not in order of citation in previous version) 26 pages; forced figures within section; corrected typos

A Proposal for a Three Detector Short-Baseline Neutrino Oscillation Program in the Fermilab Booster Neutrino Beam

Authors: R. Acciarri, C. Adams, R. An, C. Andreopoulos, A. M. Ankowski, M. Antonello, J. Asaadi, W. Badgett, L. Bagby, B. Baibussinov, B. Baller, G. Barr, N. Barros, M. Bass, V. Bellini, P. Benetti, S. Bertolucci, K. Biery, H. Bilokon, M. Bishai, A. Bitadze, A. Blake, F. Boffelli, T. Bolton, M. Bonesini , et al. (199 additional authors not shown)

Abstract: A Short-Baseline Neutrino (SBN) physics program of three LAr-TPC detectors located along the Booster Neutrino Beam (BNB) at Fermilab is presented. This new SBN Program will deliver a rich and compelling physics opportunity, including the ability to resolve a class of experimental anomalies in neutrino physics and to perform the most sensitive search to date for sterile neutrinos at the eV mass-sca… ▽ More A Short-Baseline Neutrino (SBN) physics program of three LAr-TPC detectors located along the Booster Neutrino Beam (BNB) at Fermilab is presented. This new SBN Program will deliver a rich and compelling physics opportunity, including the ability to resolve a class of experimental anomalies in neutrino physics and to perform the most sensitive search to date for sterile neutrinos at the eV mass-scale through both appearance and disappearance oscillation channels. Using data sets of 6.6e20 protons on target (P.O.T.) in the LAr1-ND and ICARUS T600 detectors plus 13.2e20 P.O.T. in the MicroBooNE detector, we estimate that a search for muon neutrino to electron neutrino appearance can be performed with ~5 sigma sensitivity for the LSND allowed (99% C.L.) parameter region. In this proposal for the SBN Program, we describe the physics analysis, the conceptual design of the LAr1-ND detector, the design and refurbishment of the T600 detector, the necessary infrastructure required to execute the program, and a possible reconfiguration of the BNB target and horn system to improve its performance for oscillation searches. △ Less

Submitted 4 March, 2015; originally announced March 2015.

Comments: 209 pages, 129 figures

Image Segmentation in Liquid Argon Time Projection Chamber Detector

Authors: Piotr Płoński, Dorota Stefan, Robert Sulej, Krzysztof Zaremba

Abstract: The Liquid Argon Time Projection Chamber (LAr-TPC) detectors provide excellent imaging and particle identification ability for studying neutrinos. An efficient and automatic reconstruction procedures are required to exploit potential of this imaging technology. Herein, a novel method for segmentation of images from LAr-TPC detectors is presented. The proposed approach computes a feature descriptor… ▽ More The Liquid Argon Time Projection Chamber (LAr-TPC) detectors provide excellent imaging and particle identification ability for studying neutrinos. An efficient and automatic reconstruction procedures are required to exploit potential of this imaging technology. Herein, a novel method for segmentation of images from LAr-TPC detectors is presented. The proposed approach computes a feature descriptor for each pixel in the image, which characterizes amplitude distribution in pixel and its neighbourhood. The supervised classifier is employed to distinguish between pixels representing particle's track and noise. The classifier is trained and evaluated on the hand-labeled dataset. The proposed approach can be a preprocessing step for reconstructing algorithms working directly on detector images. △ Less

Submitted 27 February, 2015; originally announced February 2015.

Comments: 10 pages, 4 figures, 2 tables

Some conclusive considerations on the comparison of the ICARUS nu_mu to nu_e oscillation search with the MiniBooNE low-energy event excess

Authors: M. Antonello, B. Baibussinov, P. Benetti, F. Boffelli, A. Bubak, E. Calligarich, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, A. Dermenev, A. Falcone, C. Farnese, A. Fava, A. Ferrari, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, M. Kirsanov, J. Kisiel, I. Kochanek , et al. (29 additional authors not shown)

Abstract: A sensitive search for anomalous LSND-like nu_mu to nu_e oscillations has been performed by the ICARUS Collaboration exposing the T600 LAr-TPC to the CERN to Gran Sasso (CNGS) neutrino beam. The result is compatible with the absence of additional anomalous contributions giving a limit to oscillation probability of 3.4E-3 and 7.6E-3 at 90% and 99% confidence levels respectively showing a tension be… ▽ More A sensitive search for anomalous LSND-like nu_mu to nu_e oscillations has been performed by the ICARUS Collaboration exposing the T600 LAr-TPC to the CERN to Gran Sasso (CNGS) neutrino beam. The result is compatible with the absence of additional anomalous contributions giving a limit to oscillation probability of 3.4E-3 and 7.6E-3 at 90% and 99% confidence levels respectively showing a tension between these new limits and the low-energy event excess (200 < E_nu QE < 475 MeV) reported by MiniBooNE Collaboration. A more detailed comparison of the ICARUS data with the MiniBooNE low-energy excess has been performed, including the energy resolution as obtained from the official MiniBooNE data release. As a result the previously reported tension is confirmed at 90% C.L., suggesting an unexplained nature or an otherwise instrumental effect for the MiniBooNE low energy event excess △ Less

Submitted 17 February, 2015; originally announced February 2015.

Comments: 8 pages, 8 figures

IFC Inside: Retrofitting Languages with Dynamic Information Flow Control (Extended Version)

Authors: Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, Alejandro Russo

Abstract: Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its… ▽ More Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups), may be effectively addressed using an efficient implementation of information flow control (IFC). Unfortunately existing fine-grained approaches to JavaScript IFC require modifications to the language semantics and its engine, a non-goal for browser applications. In this work, we take the ideas of coarse-grained dynamic IFC and provide the theoretical foundation for a language-based approach that can be applied to any programming language for which external effects can be controlled. We then apply this formalism to server- and client-side JavaScript, show how it generalizes to the C programming language, and connect it to the Haskell LIO system. Our methodology offers design principles for the construction of information flow control systems when isolation can easily be achieved, as well as compositional proofs for optimized concrete implementations of these systems, by relating them to their isolated variants. △ Less

Submitted 16 January, 2015; originally announced January 2015.

Comments: Extended version of POST'15 paper; 31 pages

Experimental observation of an extremely high electron lifetime with the ICARUS-T600 LAr-TPC

Authors: M. Antonello, B. Baibussinov, P. Benetti, F. Boffelli, A. Bubak, E. Calligarich, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, A. Dermenev, R. Dolfini, A. Falcone, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, M. Kirsanov , et al. (32 additional authors not shown)

Abstract: The ICARUS T600 detector, the largest liquid Argon Time Projection Chamber (LAr-TPC) realized after many years of RD activities, was installed and successfully operated for 3 years at the INFN Gran Sasso underground Laboratory. One of the most important issues was the need of an extremely low residual electronegative impurity content in the liquid Argon, in order to transport the free electrons cr… ▽ More The ICARUS T600 detector, the largest liquid Argon Time Projection Chamber (LAr-TPC) realized after many years of RD activities, was installed and successfully operated for 3 years at the INFN Gran Sasso underground Laboratory. One of the most important issues was the need of an extremely low residual electronegative impurity content in the liquid Argon, in order to transport the free electrons created by the ionizing particles with a very small attenuation along the drift path. The solutions adopted for the Argon re-circulation and purification systems have permitted to reach impressive results in terms of Argon purity and a free electron lifetime exceeding 15 ms, corresponding to about 20 parts per trillion of equivalent O2 contamination, a milestone for any future project involving LAr-TPC's and the development of higher detector mass scales. △ Less

Submitted 12 January, 2015; v1 submitted 19 September, 2014; originally announced September 2014.

Comments: to be submitted to JINST, LaTeX version

The trigger system of the ICARUS experiment for the CNGS beam

Authors: M. Antonello, B. Baibussinov, P. Benetti, F. Boffelli, A. Bubak, E. Calligarich, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, D. Dequal, A. Dermenev, R. Dolfini, A. Falcone, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek , et al. (34 additional authors not shown)

Abstract: The ICARUS T600 detector, with its 470 tons of active mass, is the largest liquid Argon TPC ever built. Operated for three years in the LNGS underground laboratory, it has collected thousands of CNGS neutrino beam interactions and cosmic ray events with energy spanning from tens of MeV to tens of GeV, with a trigger system based on scintillation light, charge signal on TPC wires and time informati… ▽ More The ICARUS T600 detector, with its 470 tons of active mass, is the largest liquid Argon TPC ever built. Operated for three years in the LNGS underground laboratory, it has collected thousands of CNGS neutrino beam interactions and cosmic ray events with energy spanning from tens of MeV to tens of GeV, with a trigger system based on scintillation light, charge signal on TPC wires and time information (for beam related events only). The performance of trigger system in terms of efficiency, background and live-time as a function of the event energy for the CNGS data taking is presented. △ Less

Submitted 8 August, 2014; v1 submitted 29 May, 2014; originally announced May 2014.

Comments: 23 pages, 23 figures. Published as M Antonello et al 2014 JINST 9 P08003

The cohomology ring of the 12-dimensional Fomin-Kirillov algebra

Authors: Dragos Stefan, Cristian Vay

Abstract: The $12$-dimensional Fomin-Kirillov algebra $FK_3$ is defined as the quadratic algebra with generators $a$, $b$ and $c$ which satisfy the relations $a^2=b^2=c^2=0$ and $ab+bc+ca=0=ba+cb+ac$. By a result of A. Milinski and H.-J. Schneider, this algebra is isomorphic to the Nichols algebra associated to the Yetter-Drinfeld module $V$, over the symmetric group $\mathbb{S}_3$, corresponding to the con… ▽ More The $12$-dimensional Fomin-Kirillov algebra $FK_3$ is defined as the quadratic algebra with generators $a$, $b$ and $c$ which satisfy the relations $a^2=b^2=c^2=0$ and $ab+bc+ca=0=ba+cb+ac$. By a result of A. Milinski and H.-J. Schneider, this algebra is isomorphic to the Nichols algebra associated to the Yetter-Drinfeld module $V$, over the symmetric group $\mathbb{S}_3$, corresponding to the conjugacy class of all transpositions and the sign representation. Exploiting this identification, we compute the cohomology ring $Ext_{FK_3}^*(\Bbbk,\Bbbk)$, showing that it is a polynomial ring $S[X]$ with coefficients in the symmetric braided algebra of $V$. As an application we also compute the cohomology rings of the bosonization $FK_3\#\Bbbk\mathbb{S}_3$ and of its dual, which are $72$-dimensional ordinary Hopf algebras. △ Less

Submitted 5 February, 2016; v1 submitted 20 April, 2014; originally announced April 2014.

Comments: v3: Final version, accepted for publication in Advances in Mathematics

Journal ref: Advances in Mathematics, Volume 291 (2016), pp. 584-620

ICARUS at FNAL

Authors: M. Antonello, B. Baibussinov, V. Bellini, H. Bilokon, F. Boffelli, M. Bonesini, E. Calligarich, S. Centro, K. Cieslik, D. B. Cline, A. G. Cocco, A. Curioni, A. Dermenev, R. Dolfini, A. Falcone, C. Farnese, A. Fava, A. Ferrari, D. Gibin, S. Gninenko, F. Guber, A. Guglielmi, M. Haranczyk, J. Holeczek, A. Ivashkin , et al. (41 additional authors not shown)

Abstract: The INFN and the ICARUS collaboration originally developed the technology of the LAr-TPC. Located the underground LNGS Hall-B, the ICARUS T600 detector has been performed over three years with remarkable detection efficiency featuring a smooth operation, high live time, and high reliability. About 3000 CNGS neutrino events have been collected and are being actively analyzed. ICARUS will now be mov… ▽ More The INFN and the ICARUS collaboration originally developed the technology of the LAr-TPC. Located the underground LNGS Hall-B, the ICARUS T600 detector has been performed over three years with remarkable detection efficiency featuring a smooth operation, high live time, and high reliability. About 3000 CNGS neutrino events have been collected and are being actively analyzed. ICARUS will now be moved to CERN for an extensive R&D program. The T600 detector will be overhauled and complemented with a similar T150 detector. These improvements are performed in collaboration with the LBNE experiment, of which several INFN Institutions are now members. As a novelty, a SC magnetic field of about 1 T will be introduced. During 2016 it is proposed to move the experiment to FNAL where short base line neutrino beams are available, complementing the approved MicroBooNe experiment which will start operation in 2014. The ICARUS detectors at FNAL will be an important addition since, in absence of anomalies, the signals of several detectors at different distances from the target should be a copy of each other for all experimental signatures. Due to the reduced mass, in MicroBooNE the anti-neutrino signal is too weak for a sensitive comparison. Hence, a definitive clarification of the LSND anomaly requires the exploration of the anti-neutrino signal provided by the much larger T600. The magnetic field will allow separating the anti-neutrino signal from the neutrino-induced background. It is proposed to expose the T600 at the Booster NuBeam at ~700 m from target; the T150 will be located at ~150 m. The T600 will also receive >10^4 nu_e events/year from the off-axis NUMI beam peaked around 1 GeV and exploitable to prepare for the LBNE experiment. The ICARUS teams are also interested in extending the participation to other short baseline neutrino activities collaborating with existing FNAL groups. △ Less

Submitted 10 January, 2014; v1 submitted 27 December, 2013; originally announced December 2013.

Comments: Experiment Proposal; 54 pages, 33 figures

The Long-Baseline Neutrino Experiment: Exploring Fundamental Symmetries of the Universe

Authors: LBNE Collaboration, Corey Adams, David Adams, Tarek Akiri, Tyler Alion, Kris Anderson, Costas Andreopoulos, Mike Andrews, Ioana Anghel, João Carlos Costa dos Anjos, Maddalena Antonello, Enrique Arrieta-Diaz, Marina Artuso, Jonathan Asaadi, Xinhua Bai, Bagdat Baibussinov, Michael Baird, Baha Balantekin, Bruce Baller, Brian Baptista, D'Ann Barker, Gary Barker, William A. Barletta, Giles Barr, Larry Bartoszek , et al. (461 additional authors not shown)

Abstract: The preponderance of matter over antimatter in the early Universe, the dynamics of the supernova bursts that produced the heavy elements necessary for life and whether protons eventually decay --- these mysteries at the forefront of particle physics and astrophysics are key to understanding the early evolution of our Universe, its current state and its eventual fate. The Long-Baseline Neutrino Exp… ▽ More The preponderance of matter over antimatter in the early Universe, the dynamics of the supernova bursts that produced the heavy elements necessary for life and whether protons eventually decay --- these mysteries at the forefront of particle physics and astrophysics are key to understanding the early evolution of our Universe, its current state and its eventual fate. The Long-Baseline Neutrino Experiment (LBNE) represents an extensively developed plan for a world-class experiment dedicated to addressing these questions. LBNE is conceived around three central components: (1) a new, high-intensity neutrino source generated from a megawatt-class proton accelerator at Fermi National Accelerator Laboratory, (2) a near neutrino detector just downstream of the source, and (3) a massive liquid argon time-projection chamber deployed as a far detector deep underground at the Sanford Underground Research Facility. This facility, located at the site of the former Homestake Mine in Lead, South Dakota, is approximately 1,300 km from the neutrino source at Fermilab -- a distance (baseline) that delivers optimal sensitivity to neutrino charge-parity symmetry violation and mass ordering effects. This ambitious yet cost-effective design incorporates scalability and flexibility and can accommodate a variety of upgrades and contributions. With its exceptional combination of experimental configuration, technical capabilities, and potential for transformative discoveries, LBNE promises to be a vital facility for the field of particle physics worldwide, providing physicists from around the globe with opportunities to collaborate in a twenty to thirty year program of exciting science. In this document we provide a comprehensive overview of LBNE's scientific objectives, its place in the landscape of neutrino physics worldwide, the technologies it will incorporate and the capabilities it will possess. △ Less

Submitted 22 April, 2014; v1 submitted 28 July, 2013; originally announced July 2013.

Comments: Major update of previous version. This is the reference document for LBNE science program and current status. Chapters 1, 3, and 9 provide a comprehensive overview of LBNE's scientific objectives, its place in the landscape of neutrino physics worldwide, the technologies it will incorporate and the capabilities it will possess. 288 pages, 116 figures

Report number: BNL-101354-2014-JA, FERMILAB-PUB-14-022, LA-UR-14-20881

Search for anomalies in the νe appearance from a νμ beam

Authors: M. Antonello, B. Baibussinov, P. Benetti, F. Boffelli, A. Bubak, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, D. Dequal, A. Dermenev, R. Dolfini, A. Falcone, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk , et al. (35 additional authors not shown)

Abstract: We report an updated result from the ICARUS experiment on the search for νμ ->νe anomalies with the CNGS beam, produced at CERN with an average energy of 20 GeV and travelling 730 km to the Gran Sasso Laboratory. The present analysis is based on a total sample of 1995 events of CNGS neutrino interactions, which corresponds to an almost doubled sample with respect to the previously published result… ▽ More We report an updated result from the ICARUS experiment on the search for νμ ->νe anomalies with the CNGS beam, produced at CERN with an average energy of 20 GeV and travelling 730 km to the Gran Sasso Laboratory. The present analysis is based on a total sample of 1995 events of CNGS neutrino interactions, which corresponds to an almost doubled sample with respect to the previously published result. Four clear νe events have been visually identified over the full sample, compared with an expectation of 6.4 +- 0.9 events from conventional sources. The result is compatible with the absence of additional anomalous contributions. At 90% and 99% confidence levels the limits to possible oscillated events are 3.7 and 8.3 respectively. The corresponding limit to oscillation probability becomes consequently 3.4 x 10-3 and 7.6 x 10-3 respectively. The present result confirms, with an improved sensitivity, the early result already published by the ICARUS collaboration. △ Less

Submitted 7 August, 2013; v1 submitted 17 July, 2013; originally announced July 2013.

Precise 3D track reconstruction algorithm for the ICARUS T600 liquid argon time projection chamber detector

Authors: M. Antonello, B. Baibussinov, P. Benetti, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, D. Dequal, A. Dermenev, R. Dolfini, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, A. Ivashkin, J. Kisiel , et al. (31 additional authors not shown)

Abstract: Liquid Argon Time Projection Chamber (LAr TPC) detectors offer charged particle imaging capability with remarkable spatial resolution. Precise event reconstruction procedures are critical in order to fully exploit the potential of this technology. In this paper we present a new, general approach of three-dimensional reconstruction for the LAr TPC with a practical application to track reconstructio… ▽ More Liquid Argon Time Projection Chamber (LAr TPC) detectors offer charged particle imaging capability with remarkable spatial resolution. Precise event reconstruction procedures are critical in order to fully exploit the potential of this technology. In this paper we present a new, general approach of three-dimensional reconstruction for the LAr TPC with a practical application to track reconstruction. The efficiency of the method is evaluated on a sample of simulated tracks. We present also the application of the method to the analysis of real data tracks collected during the ICARUS T600 detector operation with the CNGS neutrino beam. △ Less

Submitted 11 January, 2013; v1 submitted 18 October, 2012; originally announced October 2012.

Comments: Submitted to Advances in High Energy Physics

Journal ref: AHEP Volume 2013(2013), Article ID 260820

Experimental search for the LSND anomaly with the ICARUS detector in the CNGS neutrino beam

Authors: M. Antonello, B. Baibussinov, P. Benetti, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, D. Dequal, A. Dermenev, R. Dolfini, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, A. Ivashkin, J. Kisiel , et al. (32 additional authors not shown)

Abstract: We report an early result from the ICARUS experiment on the search for nu_mu to nu_e signal due to the LSND anomaly. The search was performed with the ICARUS T600 detector located at the Gran Sasso Laboratory, receiving CNGS neutrinos from CERN at an average energy of about 20 GeV, after a flight path of about 730 km. The LSND anomaly would manifest as an excess of nu_e events, characterized by a… ▽ More We report an early result from the ICARUS experiment on the search for nu_mu to nu_e signal due to the LSND anomaly. The search was performed with the ICARUS T600 detector located at the Gran Sasso Laboratory, receiving CNGS neutrinos from CERN at an average energy of about 20 GeV, after a flight path of about 730 km. The LSND anomaly would manifest as an excess of nu_e events, characterized by a fast energy oscillation averaging approximately to sin^2(1.27 Dm^2_new L/ E_nu) = 1/2. The present analysis is based on 1091 neutrino events, which are about 50% of the ICARUS data collected in 2010-2011. Two clear nu_e events have been found, compared with the expectation of 3.7 +/- 0.6 events from conventional sources. Within the range of our observations, this result is compatible with the absence of a LSND anomaly. At 90% and 99% confidence levels the limits of 3.4 and 7.3 events corresponding to oscillation probabilities of 5.4 10^-3 and 1.1 10^-2 are set respectively. The result strongly limits the window of open options for the LSND anomaly to a narrow region around (Dm^2, sin^2(2 theta))_new = (0.5 eV^2, 0.005), where there is an overall agreement (90% CL) between the present ICARUS limit, the published limits of KARMEN and the published positive signals of LSND and MiniBooNE Collaborations. △ Less

Submitted 19 February, 2013; v1 submitted 1 September, 2012; originally announced September 2012.

Comments: 10 pages, 7 figures

Precision measurement of the neutrino velocity with the ICARUS detector in the CNGS beam

Authors: M. Antonello, B. Baibussinov, F. Boffelli, P. Benetti, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, A. Dabrowska, D. Dequal, A. Dermenev, R. Dolfini, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, D. Gibin, S. Gninenko, A. Guglielmi, M. Haranczyk, J. Holeczek, A. Ivashkin , et al. (46 additional authors not shown)

Abstract: During May 2012, the CERN-CNGS neutrino beam has been operated for two weeks for a total of 1.8 10^17 pot in bunched mode, with a 3 ns narrow width proton beam bunches, separated by 100 ns. This tightly bunched beam structure allows a very accurate time of flight measurement of neutrinos from CERN to LNGS on an event-by-event basis. Both the ICARUS-T600 PMT-DAQ and the CERN-LNGS timing synchroniza… ▽ More During May 2012, the CERN-CNGS neutrino beam has been operated for two weeks for a total of 1.8 10^17 pot in bunched mode, with a 3 ns narrow width proton beam bunches, separated by 100 ns. This tightly bunched beam structure allows a very accurate time of flight measurement of neutrinos from CERN to LNGS on an event-by-event basis. Both the ICARUS-T600 PMT-DAQ and the CERN-LNGS timing synchronization have been substantially improved for this campaign, taking ad-vantage of additional independent GPS receivers, both at CERN and LNGS as well as of the deployment of the "White Rabbit" protocol both at CERN and LNGS. The ICARUS-T600 detector has collected 25 beam-associated events; the corresponding time of flight has been accurately evaluated, using all different time synchronization paths. The measured neutrino time of flight is compatible with the arrival of all events with speed equivalent to the one of light: the difference between the expected value based on the speed of light and the measured value is tof_c - tof_nu = (0.10 \pm 0.67stat. \pm 2.39syst.) ns. This result is in agreement with the value previously reported by the ICARUS collaboration, tof_c - tof_nu = (0.3 \pm 4.9stat. \pm 9.0syst.) ns, but with improved statistical and systematic errors. △ Less

Submitted 26 September, 2012; v1 submitted 13 August, 2012; originally announced August 2012.

Comments: 21 pages, 13 figures, 1 table

Search for anomalies in the neutrino sector with muon spectrometers and large LArTPC imaging detectors at CERN

Authors: M. Antonello, D. Bagliani, B. Baibussinov, H. Bilokon, F. Boffelli, M. Bonesini, E. Calligarich, N. Canci, S. Centro, A. Cesana, K. Cieslik, D. B. Cline, A. G. Cocco, D. Dequal, A. Dermenev, R. Dolfini, M. De Gerone, S. Dussoni, C. Farnese, A. Fava, A. Ferrari, G. Fiorillo, G. T. Garvey, F. Gatti, D. Gibin , et al. (114 additional authors not shown)

Abstract: A new experiment with an intense ~2 GeV neutrino beam at CERN SPS is proposed in order to definitely clarify the possible existence of additional neutrino states, as pointed out by neutrino calibration source experiments, reactor and accelerator experiments and measure the corresponding oscillation parameters. The experiment is based on two identical LAr-TPCs complemented by magnetized spectromete… ▽ More A new experiment with an intense ~2 GeV neutrino beam at CERN SPS is proposed in order to definitely clarify the possible existence of additional neutrino states, as pointed out by neutrino calibration source experiments, reactor and accelerator experiments and measure the corresponding oscillation parameters. The experiment is based on two identical LAr-TPCs complemented by magnetized spectrometers detecting electron and muon neutrino events at Far and Near positions, 1600 m and 300 m from the proton target, respectively. The ICARUS T600 detector, the largest LAr-TPC ever built with a size of about 600 ton of imaging mass, now running in the LNGS underground laboratory, will be moved at the CERN Far position. An additional 1/4 of the T600 detector (T150) will be constructed and located in the Near position. Two large area spectrometers will be placed downstream of the two LAr-TPC detectors to perform charge identification and muon momentum measurements from sub-GeV to several GeV energy range, greatly complementing the physics capabilities. This experiment will offer remarkable discovery potentialities, collecting a very large number of unbiased events both in the neutrino and antineutrino channels, largely adequate to definitely settle the origin of the observed neutrino-related anomalies. △ Less

Submitted 28 September, 2012; v1 submitted 3 August, 2012; originally announced August 2012.

Comments: Contribution to the European Strategy for Particle Physics - Open Symposium Preparatory Group, Kracow 10-12 September 2012