Showing 1–40 of 40 results for author: Maffei, M

Verifying Global Two-Safety Properties in Neural Networks with Confidence

Authors: Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic, Georg Weissenbacher

Abstract: We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundnes… ▽ More We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification. △ Less

Submitted 17 June, 2024; v1 submitted 23 May, 2024; originally announced May 2024.

Comments: Accepted at the 36th International Conference on Computer Aided Verification, 2024

Saturating a Fundamental Bound on Quantum Measurements' Accuracy

Authors: Nicolò Piccione, Maria Maffei, Andrew N. Jordan, Kater W. Murch, Alexia Auffèves

Abstract: A quantum system is usually measured through observations performed on a second quantum system, or meter, to which it is coupled. In this scenario, fundamental limitations arise as stated by the celebrated Wigner-Araki-Yanase theorem and its generalizations, predicting an upper-bound on the measurement's accuracy (Ozawa's bound). Here, we show it is possible to saturate this fundamental bound. We… ▽ More A quantum system is usually measured through observations performed on a second quantum system, or meter, to which it is coupled. In this scenario, fundamental limitations arise as stated by the celebrated Wigner-Araki-Yanase theorem and its generalizations, predicting an upper-bound on the measurement's accuracy (Ozawa's bound). Here, we show it is possible to saturate this fundamental bound. We propose a simple interferometric setup, arguably within reach of present technology, in which a flying particle (the quantum meter) is used to measure the state of a qubit (the target system). We show that the bound can be saturated and that this happens only if the flying particle is prepared in a Gaussian wavepacket. △ Less

Submitted 19 April, 2024; originally announced April 2024.

Comments: 5 pages plus supplemental. 2 Figures

Closing Optical Bloch Equations in waveguide QED: Dynamics, Energetics

Authors: Samyak Pratyush Prasad, Maria Maffei, Patrice A. Camati, Cyril Elouard, Alexia Auffèves

Abstract: Optical Bloch Equations (OBE) model the dynamics of a classically driven two-level atom coupled to a thermal electromagnetic field. From a global viewpoint, they derive from the unitary evolution of a closed, isolated atom-field system. We study the emergence of the OBE in the case where the driving and the thermal fields are confined in one spatial dimension -- a situation usually found in wavegu… ▽ More Optical Bloch Equations (OBE) model the dynamics of a classically driven two-level atom coupled to a thermal electromagnetic field. From a global viewpoint, they derive from the unitary evolution of a closed, isolated atom-field system. We study the emergence of the OBE in the case where the driving and the thermal fields are confined in one spatial dimension -- a situation usually found in waveguide-QED. The joint atom-field system forms a "one-dimensional atom" (1D atom) whose closed dynamics can be solved, providing access to light-matter correlations. Such closure of the OBE unveils a new term capturing the driving of the atom by itself, or self-drive, which is proportional to the atom coherences in the energy basis. A 1D atom also constitutes an autonomous, energy-conserving system. Hence, energy exchanges between the atom and the field can be conveniently analyzed as closed first laws, where work-like (heat-like) flows stem from effective unitaries (correlations) exerted by one system on the other. We show that the closed and the open approaches only differ by the atom self-work, which yields a tighter expression of the second law. We quantitatively relate this tightening to the extra-knowledge acquired by closing the OBE. The concepts and effects we introduce deepen our understanding of thermodynamics in the quantum regime and its potential for energy management at quantum scales. They can be probed in state-of-the-art quantum hardware, e.g. superconducting and photonic circuits. △ Less

Submitted 22 April, 2024; v1 submitted 15 April, 2024; originally announced April 2024.

Comments: 15+16 pages, 2 figures. Comments are welcome!

Directional emission and photon bunching from a qubit pair in waveguide

Authors: M. Maffei, D. Pomarico, P. Facchi, G. Magnifico, S. Pascazio, F. Pepe

Abstract: Waveguide quantum electrodynamics represents a powerful platform to generate entanglement and tailor photonic states. We consider a pair of identical qubits coupled to a parity invariant waveguide in the microwave domain. By working in the one- and two-excitation sectors, we provide a unified view of decay processes and we show the common origin of directional single photon emission and two photon… ▽ More Waveguide quantum electrodynamics represents a powerful platform to generate entanglement and tailor photonic states. We consider a pair of identical qubits coupled to a parity invariant waveguide in the microwave domain. By working in the one- and two-excitation sectors, we provide a unified view of decay processes and we show the common origin of directional single photon emission and two photon directional bunching. Unveiling the quantum trajectories, we demonstrate that both phenomena are rooted in the selective coupling of orthogonal qubits Bell states with different photon propagation directions. We comment on how to use this mechanism to implement optimized post-selection of Bell states, heralded by the detection of photons on one qubits side. △ Less

Submitted 2 February, 2024; originally announced February 2024.

Quantum energetics of a non-commuting measurement

Authors: Xiayu Linpeng, Nicolò Piccione, Maria Maffei, Léa Bresque, Samyak P. Prasad, Andrew N. Jordan, Alexia Auffèves, Kater W. Murch

Abstract: When a measurement observable does not commute with a quantum system's Hamiltonian, the energy of the measured system is typically not conserved during the measurement. Instead, energy can be transferred between the measured system and the meter. In this work, we experimentally investigate the energetics of non-commuting measurements in a circuit quantum electrodynamics system containing a transmo… ▽ More When a measurement observable does not commute with a quantum system's Hamiltonian, the energy of the measured system is typically not conserved during the measurement. Instead, energy can be transferred between the measured system and the meter. In this work, we experimentally investigate the energetics of non-commuting measurements in a circuit quantum electrodynamics system containing a transmon qubit embedded in a 3D microwave cavity. We show through spectral analysis of the cavity photons that a frequency shift is imparted on the probe, in balance with the associated energy changes of the qubit. Our experiment provides new insights into foundations of quantum measurement, as well as a better understanding of the key mechanisms at play in quantum energetics. △ Less

Submitted 27 November, 2023; v1 submitted 22 November, 2023; originally announced November 2023.

Comments: 9 pages, 4 figures

Fundamental mechanisms of energy exchanges in autonomous measurements based on dispersive qubit-light interaction

Authors: Nicolò Piccione, Maria Maffei, Xiayu Linpeng, Andrew N. Jordan, Kater W. Murch, Alexia Auffèves

Abstract: Measuring an observable which does not commute with the Hamiltonian of a quantum system usually modifies the mean energy of this system. In an autonomous measurement scheme, coupling the system to a quantum meter, the system's energy change must be compensated by the meter's energy change. Here, we theoretically study such an autonomous meter-system dynamics: a qubit interacting dispersively with… ▽ More Measuring an observable which does not commute with the Hamiltonian of a quantum system usually modifies the mean energy of this system. In an autonomous measurement scheme, coupling the system to a quantum meter, the system's energy change must be compensated by the meter's energy change. Here, we theoretically study such an autonomous meter-system dynamics: a qubit interacting dispersively with a light pulse propagating in a one-dimensional waveguide. The phase of the light pulse is shifted, conditioned to the qubit's state along the $z$-direction, while the orientation of the qubit Hamiltonian is arbitrary. As the interaction is dispersive, photon number is conserved so that energy balance has to be attained by spectral deformations of the light pulse. Building on analytical and numerical solutions, we reveal the mechanism underlying this spectral deformation and display how it compensates for the qubit's energy change. We explain the formation of a three-peak structure of the output spectrum and we provide the conditions under which this is observable. △ Less

Submitted 3 July, 2024; v1 submitted 20 November, 2023; originally announced November 2023.

Comments: 9 pages plus appendices, 9 figures

Journal ref: Phys. Rev. A 109, 063707 (2024)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model

Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson

Abstract: Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guaran… ▽ More Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel. △ Less

Submitted 5 April, 2024; v1 submitted 20 May, 2023; originally announced May 2023.

Anomalous energy exchanges and Wigner function negativities in a single qubit gate

Authors: Maria Maffei, Cyril Elouard, Bruno O. Goes, Benjamin Huard, Andrew N. Jordan, Alexia Auffèves

Abstract: Anomalous weak values and Wigner function's negativity are well known witnesses of quantum contextuality. We show that these effects occur when analyzing the energetics of a single qubit gate generated by a resonant coherent field traveling in a waveguide. The buildup of correlations between the qubit and the field is responsible for bounds on the gate fidelity, but also for a nontrivial energy ba… ▽ More Anomalous weak values and Wigner function's negativity are well known witnesses of quantum contextuality. We show that these effects occur when analyzing the energetics of a single qubit gate generated by a resonant coherent field traveling in a waveguide. The buildup of correlations between the qubit and the field is responsible for bounds on the gate fidelity, but also for a nontrivial energy balance recently observed in a superconducting setup. In the experimental scheme, the field is continuously monitored through heterodyne detection and then post-selected over the outcomes of a final qubit's measurement. The post-selected data can be interpreted as field's weak values and can show anomalous values in the variation of the field's energy. We model the joint system dynamics with a collision model, gaining access to the qubit-field entangled state at any time. We find an analytical expression of the quasi-probability distribution of the post-selected heterodyne signal, i.e. the conditional Husimi-Q function. The latter grants access to all the field's weak values: we use it to obtain that of the field's energy change and display its anomalous behaviour. Finally, we derive the field's conditional Wigner function and show that anomalous weak values and Wigner function's negativities arise for the same values of the gate's angle. △ Less

Submitted 11 October, 2022; originally announced October 2022.

Comments: 8 pages, 3 figures

Energy-efficient quantum non-demolition measurement with a spin-photon interface

Authors: Maria Maffei, Bruno O. Goes, Stephen C. Wein, Andrew N. Jordan, Loïc Lanco, Alexia Auffèves

Abstract: Spin-photon interfaces (SPIs) are key devices of quantum technologies, aimed at coherently transferring quantum information between spin qubits and propagating pulses of polarized light. We study the potential of a SPI for quantum non demolition (QND) measurements of a spin state. After being initialized and scattered by the SPI, the state of a light pulse depends on the spin state. It thus plays… ▽ More Spin-photon interfaces (SPIs) are key devices of quantum technologies, aimed at coherently transferring quantum information between spin qubits and propagating pulses of polarized light. We study the potential of a SPI for quantum non demolition (QND) measurements of a spin state. After being initialized and scattered by the SPI, the state of a light pulse depends on the spin state. It thus plays the role of a pointer state, information being encoded in the light's temporal and polarization degrees of freedom. Building on the fully Hamiltonian resolution of the spin-light dynamics, we show that quantum superpositions of zero and single photon states outperform coherent pulses of light, producing pointer states which are more distinguishable with the same photon budget. The energetic advantage provided by quantum pulses over coherent ones is maintained when information on the spin state is extracted at the classical level by performing projective measurements on the light pulses. The proposed schemes are robust against imperfections in state of the art semi-conducting devices. △ Less

Submitted 30 August, 2023; v1 submitted 19 May, 2022; originally announced May 2022.

Comments: Accepted for publication in Quantum

Journal ref: Quantum 7, 1099 (2023)

Energetic cost of measurements using quantum, coherent, and thermal light

Authors: Xiayu Linpeng, Léa Bresque, Maria Maffei, Andrew N. Jordan, Alexia Auffèves, Kater W. Murch

Abstract: Quantum measurements are basic operations that play a critical role in the study and application of quantum information. We study how the use of quantum, coherent, and classical thermal states of light in a circuit quantum electrodynamics setup impacts the performance of quantum measurements, by comparing their respective measurement backaction and measurement signal to noise ratio per photon. In… ▽ More Quantum measurements are basic operations that play a critical role in the study and application of quantum information. We study how the use of quantum, coherent, and classical thermal states of light in a circuit quantum electrodynamics setup impacts the performance of quantum measurements, by comparing their respective measurement backaction and measurement signal to noise ratio per photon. In the strong dispersive limit, we find that thermal light is capable of performing quantum measurements with comparable efficiency to coherent light, both being outperformed by single-photon light. We then analyze the thermodynamic cost of each measurement scheme. We show that single-photon light shows an advantage in terms of energy cost per information gain, reaching the fundamental thermodynamic cost. △ Less

Submitted 6 June, 2022; v1 submitted 2 March, 2022; originally announced March 2022.

Comments: 15 pages, 7 figures

Journal ref: Phys. Rev. Lett. 128, 220506 (2022)

Experimental analysis of energy transfers between a quantum emitter and light fields

Authors: I. Maillette de Buy Wenniger, S. E. Thomas, M. Maffei, S. C. Wein, M. Pont, N. Belabas, S. Prasad, A. Harouri, A. Lemaître, I. Sagnes, N. Somaschi, A. Auffèves, P. Senellart

Abstract: Energy transfer between quantum systems can either be achieved through an effective unitary interaction or through the generation of entanglement. This observation defines two types of energy exchange: unitary and correlation energy. Here we propose and implement experimental protocols to access these energy transfers in interactions between a quantum emitter and light fields. Upon spontaneous emi… ▽ More Energy transfer between quantum systems can either be achieved through an effective unitary interaction or through the generation of entanglement. This observation defines two types of energy exchange: unitary and correlation energy. Here we propose and implement experimental protocols to access these energy transfers in interactions between a quantum emitter and light fields. Upon spontaneous emission, we measure the unitary energy transfer from the emitter to the optical field and show that it never exceeds half of the total energy and is reduced when introducing decoherence. We then study the interference of the emitted field and a laser field at a beam splitter and show that the energy transfers quantitatively depend on the quantum purity of the emitted field. △ Less

Submitted 6 June, 2023; v1 submitted 2 February, 2022; originally announced February 2022.

WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms

Authors: Lorenzo Veronese, Benjamin Farinier, Pedro Bernardo, Mauro Tempesta, Marco Squarcina, Matteo Maffei

Abstract: The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the… ▽ More The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers. We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform. △ Less

Submitted 1 September, 2022; v1 submitted 5 January, 2022; originally announced January 2022.

Comments: Submitted to IEEE S&P '23 on 19 Aug 2022

Closed-System Solution of the 1D Atom from Collision Model

Authors: Maria Maffei, Patrice A. Camati, Alexia Auffèves

Abstract: Obtaining the total wavefunction evolution of interacting quantum systems provides access to important properties, such as entanglement, shedding light on fundamental aspects, e.g. quantum energetics and thermodynamics, and guiding towards possible application in the fields of quantum computation and communication. We consider a two-level atom (qubit) coupled to the continuum of travelling modes o… ▽ More Obtaining the total wavefunction evolution of interacting quantum systems provides access to important properties, such as entanglement, shedding light on fundamental aspects, e.g. quantum energetics and thermodynamics, and guiding towards possible application in the fields of quantum computation and communication. We consider a two-level atom (qubit) coupled to the continuum of travelling modes of a field confined in a one-dimensional waveguide. Originally, we treat the light-matter ensemble as a closed, isolated system. We solve its dynamics using a collision model where individual temporal modes of the field locally interact with the qubit in a sequential fashion. This approach allows us to obtain the total wavefunction of the qubit-field system, at any time, when the field starts in a coherent or a single-photon state. Our method is general and can be applied to other initial field states. △ Less

Submitted 17 December, 2021; originally announced December 2021.

Adoption and Actual Privacy of Decentralized CoinJoin Implementations in Bitcoin

Authors: Rainer Stütz, Johann Stockinger, Bernhard Haslhofer, Pedro Moreno-Sanchez, Matteo Maffei

Abstract: We present a first measurement study on the adoption and actual privacy of two popular decentralized CoinJoin implementations, Wasabi and Samourai, in the broader Bitcoin ecosystem. By applying highly accurate (> 99%) algorithms we can effectively detect 30,251 Wasabi and 223,597 Samourai transactions within the block range 530,500 to 725,348 (2018-07-05 to 2022-02-28). We also found a steady adop… ▽ More We present a first measurement study on the adoption and actual privacy of two popular decentralized CoinJoin implementations, Wasabi and Samourai, in the broader Bitcoin ecosystem. By applying highly accurate (> 99%) algorithms we can effectively detect 30,251 Wasabi and 223,597 Samourai transactions within the block range 530,500 to 725,348 (2018-07-05 to 2022-02-28). We also found a steady adoption of these services with a total value of mixed coins of ca. 4.74 B USD and average monthly mixing amounts of ca. 172.93 M USD) for Wasabi and ca. 41.72 M USD for Samourai. Furthermore, we could trace ca. 322 M USD directly received by cryptoasset exchanges and ca. 1.16 B USD indirectly received via two hops. Our analysis further shows that the traceability of addresses during the pre-mixing and post-mixing narrows down the anonymity set provided by these coin mixing services. It also shows that the selection of addresses for the CoinJoin transaction can harm anonymity. Overall, this is the first paper to provide a comprehensive picture of the adoption and privacy of distributed CoinJoin transactions. Understanding this picture is particularly interesting in the light of ongoing regulatory efforts that will, on the one hand, affect compliance measures implemented in cryptocurrency exchanges and, on the other hand, the privacy of end-users. △ Less

Submitted 14 September, 2022; v1 submitted 21 September, 2021; originally announced September 2021.

Energetics of a Single Qubit Gate

Authors: Jeremy Stevens, Daniel Szombati, Maria Maffei, Cyril Elouard, Réouven Assouly, Nathanaël Cottet, Rémy Dassonneville, Quentin Ficheux, Stefan Zeppetzauer, Audrey Bienfait, Andrew N. Jordan, Alexia Auffèves, Benjamin Huard

Abstract: Qubits are physical, a quantum gate thus not only acts on the information carried by the qubit but also on its energy. What is then the corresponding flow of energy between the qubit and the controller that implements the gate? Here we exploit a superconducting platform to answer this question in the case of a quantum gate realized by a resonant drive field. During the gate, the superconducting qu… ▽ More Qubits are physical, a quantum gate thus not only acts on the information carried by the qubit but also on its energy. What is then the corresponding flow of energy between the qubit and the controller that implements the gate? Here we exploit a superconducting platform to answer this question in the case of a quantum gate realized by a resonant drive field. During the gate, the superconducting qubit becomes entangled with the microwave drive pulse so that there is a quantum superposition between energy flows. We measure the energy change in the drive field conditioned on the outcome of a projective qubit measurement. We demonstrate that the drive's energy change associated with the measurement backaction can exceed by far the energy that can be extracted by the qubit. This can be understood by considering the qubit as a weak measurement apparatus of the driving field. △ Less

Submitted 24 August, 2022; v1 submitted 20 September, 2021; originally announced September 2021.

Journal ref: Physical Review Letters, 129, 110601 (2022)

Towards a Game-Theoretic Security Analysis of Off-Chain Protocols

Authors: Sophie Rain, Georgia Avarikioti, Laura Kovács, Matteo Maffei

Abstract: Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of p… ▽ More Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network. △ Less

Submitted 24 October, 2022; v1 submitted 15 September, 2021; originally announced September 2021.

Comments: This submission is the extended version of our CSF 2023 paper "Towards a Game-Theoretic Security Analysis of Off-Chain Protocols"

Linking topological features of the Hofstadter model to optical diffraction figures

Authors: Francesco Di Colandrea, Alessio D'Errico, Maria Maffei, Hannah M. Price, Maciej Lewenstein, Lorenzo Marrucci, Filippo Cardano, Alexandre Dauphin, Pietro Massignan

Abstract: In two, three and even four spatial dimensions, the transverse responses experienced by a charged particle on a lattice in a uniform magnetic field are fully controlled by topological invariants called Chern numbers, which characterize the energy bands of the underlying Hofstadter Hamiltonian. These remarkable features, solely arising from the magnetic translational symmetry, are captured by Dioph… ▽ More In two, three and even four spatial dimensions, the transverse responses experienced by a charged particle on a lattice in a uniform magnetic field are fully controlled by topological invariants called Chern numbers, which characterize the energy bands of the underlying Hofstadter Hamiltonian. These remarkable features, solely arising from the magnetic translational symmetry, are captured by Diophantine equations which relate the fraction of occupied states, the magnetic flux and the Chern numbers of the system bands. Here we investigate the close analogy between the topological properties of Hofstadter Hamiltonians and the diffraction figures resulting from optical gratings. In particular, we show that there is a one-to-one relation between the above mentioned Diophantine equation and the Bragg condition determining the far-field positions of the optical diffraction peaks. As an interesting consequence of this map**, we discuss how the robustness of diffraction figures to structural disorder in the grating is a direct analogue of the robustness of transverse conductance in the Quantum Hall effect. △ Less

Submitted 27 January, 2022; v1 submitted 16 June, 2021; originally announced June 2021.

Journal ref: New J. Phys. 24 (2022) 013028

Photon-number entanglement generated by sequential excitation of a two-level atom

Authors: S. C. Wein, J. C. Loredo, M. Maffei, P. Hilaire, A. Harouri, N. Somaschi, A. Lemaître, I. Sagnes, L. Lanco, O. Krebs, A. Auffèves, C. Simon, P. Senellart, C. Antón-Solanas

Abstract: Entanglement and spontaneous emission are fundamental quantum phenomena that drive many applications of quantum physics. During the spontaneous emission of light from an excited two-level atom, the atom briefly becomes entangled with the photonic field. Here, we show that this natural process can be used to produce photon-number entangled states of light distributed in time. By exciting a quantum… ▽ More Entanglement and spontaneous emission are fundamental quantum phenomena that drive many applications of quantum physics. During the spontaneous emission of light from an excited two-level atom, the atom briefly becomes entangled with the photonic field. Here, we show that this natural process can be used to produce photon-number entangled states of light distributed in time. By exciting a quantum dot -- an artificial two-level atom -- with two sequential $π$ pulses, we generate a photon-number Bell state. We characterise this state using time-resolved intensity and phase correlation measurements. Furthermore, we theoretically show that applying longer sequences of pulses to a two-level atom can produce a series of multi-temporal mode entangled states with properties intrinsically related to the Fibonacci sequence. Our results on photon-number entanglement can be further exploited to generate new states of quantum light with applications in quantum technologies. △ Less

Submitted 8 April, 2022; v1 submitted 3 June, 2021; originally announced June 2021.

Comments: Main: 7 pages, 3 figures; Supplementary: 15 pages, 7 figures

Probing non-classical light fields with energetic witnesses in Waveguide Quantum Electro-Dynamics

Authors: Maria Maffei, Patrice A. Camati, Alexia Auffèves

Abstract: We analyze energy exchanges between a qubit and a resonant field propagating in a waveguide. The joint dynamics is analytically solved within a repeated interaction model. The work received by the qubit is defined as the unitary component of the field-induced energy change. Using the same definition for the field, we show that both work flows compensate each other. Focusing on the charging of a qu… ▽ More We analyze energy exchanges between a qubit and a resonant field propagating in a waveguide. The joint dynamics is analytically solved within a repeated interaction model. The work received by the qubit is defined as the unitary component of the field-induced energy change. Using the same definition for the field, we show that both work flows compensate each other. Focusing on the charging of a qubit battery by a pulse of light, we evidence that the work provided by a coherent field is an upper bound for the qubit ergotropy, while this bound can be violated by non-classical fields, e.g. a coherent superposition of zero- and single-photon states. Our results provide operational, energy-based witnesses to probe the non-classical nature of a light field. △ Less

Submitted 27 September, 2021; v1 submitted 11 February, 2021; originally announced February 2021.

Comments: Considerably re-structured; closer to the published version

Journal ref: Phys. Rev. Research 3, 032073 (2021)

The Good, the Bad and the Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts

Authors: Clara Schneidewind, Markus Scherer, Matteo Maffei

Abstract: Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We revie… ▽ More Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works. △ Less

Submitted 14 January, 2021; originally announced January 2021.

Can I Take Your Subdomain? Exploring Related-Domain Attacks in the Modern Web

Authors: Marco Squarcina, Mauro Tempesta, Lorenzo Veronese, Stefano Calzavara, Matteo Maffei

Abstract: Related-domain attackers control a sibling domain of their target web application, e.g., as the result of a subdomain takeover. Despite their additional power over traditional web attackers, related-domain attackers received only limited attention by the research community. In this paper we define and quantify for the first time the threats that related-domain attackers pose to web application sec… ▽ More Related-domain attackers control a sibling domain of their target web application, e.g., as the result of a subdomain takeover. Despite their additional power over traditional web attackers, related-domain attackers received only limited attention by the research community. In this paper we define and quantify for the first time the threats that related-domain attackers pose to web application security. In particular, we first clarify the capabilities that related-domain attackers can acquire through different attack vectors, showing that different instances of the related-domain attacker concept are worth attention. We then study how these capabilities can be abused to compromise web application security by focusing on different angles, including: cookies, CSP, CORS, postMessage and domain relaxation. By building on this framework, we report on a large-scale security measurement on the top 50k domains from the Tranco list that led to the discovery of vulnerabilities in 887 sites, where we quantified the threats posed by related-domain attackers to popular web applications. △ Less

Submitted 3 December, 2020; originally announced December 2020.

Comments: Submitted to USENIX Security '21 on 16 Oct 2020

Optimizing Virtual Payment Channel Establishment in the Face of On-Path Adversaries

Authors: Lukas Aumayr, Esra Ceylan, Yannik Kopyciok, Matteo Maffei, Pedro Moreno-Sanchez, Iosif Salem, Stefan Schmid

Abstract: Payment channel networks (PCNs) are among the most promising solutions to the scalability issues in permissionless blockchains, by allowing parties to pay each other off-chain through a path of payment channels (PCs). However, routing transactions comes at a cost which is proportional to the number of intermediaries, since each charges a fee for the routing service. Furthermore, analogous to other… ▽ More Payment channel networks (PCNs) are among the most promising solutions to the scalability issues in permissionless blockchains, by allowing parties to pay each other off-chain through a path of payment channels (PCs). However, routing transactions comes at a cost which is proportional to the number of intermediaries, since each charges a fee for the routing service. Furthermore, analogous to other networks, malicious intermediaries in the payment path can lead to security and privacy threats. Virtual channels (VCs), i.e., bridges over PC paths, mitigate the above PCN issues, as an intermediary participates only once to set up the VC and is then excluded from every future VC transaction. However, similar to PCs, creating a VC has a cost that must be paid out of the bridged PCs' balance. Currently, we are missing guidelines to where and how many VCs to set up. Ideally, VCs should minimize transaction costs while mitigating security and privacy threats from on-path adversaries. In this work, we address for the first time the VC setup problem, formalizing it as an optimization problem. We present an integer linear program (ILP) to compute the globally optimal VC setup strategy in terms of transaction costs, security, and privacy. We then accompany the computationally heavy ILP with a fast local greedy algorithm. Our model and algorithms can be used with any on-path adversary, given that its strategy can be expressed as a set of corrupted nodes that is estimated by the honest nodes. We conduct an evaluation of the greedy algorithm over a snapshot of the Lightning Network (LN), the largest Bitcoin-based PCN. Our results confirm on real-world data that our greedy strategy minimizes costs while protecting against security and privacy threats of on-path adversaries. These findings may serve the LN community as guidelines for the deployment of VCs. △ Less

Submitted 9 May, 2024; v1 submitted 29 November, 2020; originally announced November 2020.

Comments: This is the extended technical report of the work accepted at IFIP Networking 2024

Cross-Layer Deanonymization Methods in the Lightning Protocol

Authors: Matteo Romiti, Friedhelm Victor, Pedro Moreno-Sanchez, Peter Sebastian Nordholt, Bernhard Haslhofer, Matteo Maffei

Abstract: Bitcoin (BTC) pseudonyms (layer 1) can effectively be deanonymized using heuristic clustering techniques. However, while performing transactions off-chain (layer 2) in the Lightning Network (LN) seems to enhance privacy, a systematic analysis of the anonymity and privacy leakages due to the interaction between the two layers is missing. We present clustering heuristics that group BTC addresses, ba… ▽ More Bitcoin (BTC) pseudonyms (layer 1) can effectively be deanonymized using heuristic clustering techniques. However, while performing transactions off-chain (layer 2) in the Lightning Network (LN) seems to enhance privacy, a systematic analysis of the anonymity and privacy leakages due to the interaction between the two layers is missing. We present clustering heuristics that group BTC addresses, based on their interaction with the LN, as well as LN nodes, based on shared naming and hosting information. We also present linking heuristics that link 45.97% of all LN nodes to 29.61% BTC addresses interacting with the LN. These links allow us to attribute information (e.g., aliases, IP addresses) to 21.19% of the BTC addresses contributing to their deanonymization. Further, these deanonymization results suggest that the security and privacy of LN payments are weaker than commonly believed, with LN users being at the mercy of as few as five actors that control 36 nodes and over 33% of the total capacity. Overall, this is the first paper to present a method for linking LN nodes with BTC addresses across layers and to discuss privacy and security implications. △ Less

Submitted 10 February, 2021; v1 submitted 1 July, 2020; originally announced July 2020.

Comments: 30 pages, 9 figures, Financial Cryptography and Data Security 2021 https://fc21.ifca.ai/

eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

Authors: Clara Schneidewind, Ilya Grishchenko, Markus Scherer, Matteo Maffei

Abstract: Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blo… ▽ More Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%. △ Less

Submitted 13 May, 2020; originally announced May 2020.

Comments: Accepted for CCS 2020

Language-Based Web Session Integrity

Authors: Stefano Calzavara, Riccardo Focardi, Niklas Grimm, Matteo Maffei, Mauro Tempesta

Abstract: Session management is a fundamental component of web applications: despite the apparent simplicity, correctly implementing web sessions is extremely tricky, as witnessed by the large number of existing attacks. This motivated the design of formal methods to rigorously reason about web session security which, however, are not supported at present by suitable automated verification techniques. In th… ▽ More Session management is a fundamental component of web applications: despite the apparent simplicity, correctly implementing web sessions is extremely tricky, as witnessed by the large number of existing attacks. This motivated the design of formal methods to rigorously reason about web session security which, however, are not supported at present by suitable automated verification techniques. In this paper we introduce the first security type system that enforces session security on a core model of web applications, focusing in particular on server-side code. We showcase the expressiveness of our type system by analyzing the session management logic of HotCRP, Moodle, and phpMyAdmin, unveiling novel security flaws that have been acknowledged by software developers. △ Less

Submitted 2 June, 2020; v1 submitted 28 January, 2020; originally announced January 2020.

Concurrency and Privacy with Payment-Channel Networks

Authors: Giulio Malavolta, Pedro Moreno-Sanchez, Aniket Kate, Matteo Maffei, Srivatsan Ravi

Abstract: Permissionless blockchains protocols such as Bitcoin are inherently limited in transaction throughput and latency. Current efforts to address this key issue focus on off-chain payment channels that can be combined in a Payment-Channel Network (PCN) to enable an unlimited number of payments without requiring to access the blockchain other than to register the initial and final capacity of each chan… ▽ More Permissionless blockchains protocols such as Bitcoin are inherently limited in transaction throughput and latency. Current efforts to address this key issue focus on off-chain payment channels that can be combined in a Payment-Channel Network (PCN) to enable an unlimited number of payments without requiring to access the blockchain other than to register the initial and final capacity of each channel. While this approach paves the way for low latency and high throughput of payments, its deployment in practice raises several privacy concerns as well as technical challenges related to the inherently concurrent nature of payments, such as race conditions and deadlocks, that have been understudied so far. In this work, we lay the foundations for privacy and concurrency in PCNs, presenting a formal definition in the Universal Composability framework as well as practical and provably secure solutions. In particular, we present Fulgor and Rayo. Fulgor is the first payment protocol for PCNs that provides provable privacy guarantees for PCNs and is fully compatible with the Bitcoin scripting system. However, Fulgor is a blocking protocol and therefore prone to deadlocks of concurrent payments as in currently available PCNs. Instead, Rayo is the first protocol for PCNs that enforces non-blocking progress (i.e., at least one of the concurrent payments terminates). We show through a new impossibility result that non-blocking progress necessarily comes at the cost of weaker privacy. At the core of Fulgor and Rayo is Multi-Hop HTLC, a new smart contract, compatible with the Bitcoin scripting system, that provides conditional payments while reducing running time and communication overhead with respect to previous approaches. △ Less

Submitted 20 November, 2019; originally announced November 2019.

Verifying Relational Properties using Trace Logic

Authors: Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs, Matteo Maffei

Abstract: We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive inst… ▽ More We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive instance of first-order predicate logic. Trace logic draws its expressiveness from its syntax, which allows expressing properties over computation traces. Its axiomatization supports fine-grained reasoning about intermediate steps in program execution, notably loop iterations. We present an algorithm to encode the semantics of programs as well as their relational properties in trace logic, and then show how first-order theorem proving can be used to reason about the resulting trace logic formulas. Our work is implemented in the tool Rapid and evaluated with examples coming from the security field. △ Less

Submitted 12 August, 2019; v1 submitted 24 June, 2019; originally announced June 2019.

Two-dimensional topological quantum walks in the momentum space of structured light

Authors: Alessio D'Errico, Filippo Cardano, Maria Maffei, Alexandre Dauphin, Raouf Barboza, Chiara Esposito, Bruno Piccirillo, Maciej Lewenstein, Pietro Massignan, Lorenzo Marrucci

Abstract: Quantum walks are powerful tools for quantum applications and for designing topological systems. Although they are simulated in a variety of platforms, genuine two-dimensional realizations are still challenging. Here we present an innovative approach to the photonic simulation of a quantum walk in two dimensions, where walker positions are encoded in the transverse wavevector components of a singl… ▽ More Quantum walks are powerful tools for quantum applications and for designing topological systems. Although they are simulated in a variety of platforms, genuine two-dimensional realizations are still challenging. Here we present an innovative approach to the photonic simulation of a quantum walk in two dimensions, where walker positions are encoded in the transverse wavevector components of a single light beam. The desired dynamics is obtained by means of a sequence of liquid-crystal devices, which apply polarization-dependent transverse "kicks" to the photons in the beam. We engineer our quantum walk so that it realizes a periodically-driven Chern insulator, and we probe its topological features by detecting the anomalous displacement of the photonic wavepacket under the effect of a constant force. Our compact, versatile platform offers exciting prospects for the photonic simulation of two-dimensional quantum dynamics and topological systems. △ Less

Submitted 6 February, 2020; v1 submitted 9 November, 2018; originally announced November 2018.

Comments: Published version of the manuscript

Journal ref: Optica, vol. 7, issue 2, pp. 108-114 (2020)

WPSE: Fortifying Web Protocols via Browser-Side Security Monitoring

Authors: Stefano Calzavara, Riccardo Focardi, Matteo Maffei, Clara Schneidewind, Marco Squarcina, Mauro Tempesta

Abstract: We present WPSE, a browser-side security monitor for web protocols designed to ensure compliance with the intended protocol flow, as well as confidentiality and integrity properties of messages. We formally prove that WPSE is expressive enough to protect web applications from a wide range of protocol implementation bugs and web attacks. We discuss concrete examples of attacks which can be prevente… ▽ More We present WPSE, a browser-side security monitor for web protocols designed to ensure compliance with the intended protocol flow, as well as confidentiality and integrity properties of messages. We formally prove that WPSE is expressive enough to protect web applications from a wide range of protocol implementation bugs and web attacks. We discuss concrete examples of attacks which can be prevented by WPSE on OAuth 2.0 and SAML 2.0, including a novel attack on the Google implementation of SAML 2.0 which we discovered by formalizing the protocol specification in WPSE. Moreover, we use WPSE to carry out an extensive experimental evaluation of OAuth 2.0 in the wild. Out of 90 tested websites, we identify security flaws in 55 websites (61.1%), including new critical vulnerabilities introduced by tracking libraries such as Facebook Pixel, all of which fixable by WPSE. Finally, we show that WPSE works flawlessly on 83 websites (92.2%), with the 7 compatibility issues being caused by custom implementations deviating from the OAuth 2.0 specification, one of which introducing a critical vulnerability. △ Less

Submitted 24 June, 2018; originally announced June 2018.

A Semantic Framework for the Security Analysis of Ethereum smart contracts

Authors: Ilya Grishchenko, Matteo Maffei, Clara Schneidewind

Abstract: Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent a… ▽ More Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques. △ Less

Submitted 23 April, 2018; v1 submitted 23 February, 2018; originally announced February 2018.

Comments: The EAPLS Best Paper Award at ETAPS

Journal ref: POST 2018: 243-269

Observation of the topological Anderson insulator in disordered atomic wires

Authors: Eric J. Meier, Fangzhao Alex An, Alexandre Dauphin, Maria Maffei, Pietro Massignan, Taylor L. Hughes, Bryce Gadway

Abstract: Topology and disorder have deep connections and a rich combined influence on quantum transport. In order to probe these connections, we synthesized one-dimensional chiral symmetric wires with controllable disorder via spectroscopic Hamiltonian engineering, based on the laser-driven coupling of discrete momentum states of ultracold atoms. We characterize the system's topology through measurement of… ▽ More Topology and disorder have deep connections and a rich combined influence on quantum transport. In order to probe these connections, we synthesized one-dimensional chiral symmetric wires with controllable disorder via spectroscopic Hamiltonian engineering, based on the laser-driven coupling of discrete momentum states of ultracold atoms. We characterize the system's topology through measurement of the mean chiral displacement of the bulk density extracted from quench dynamics. We find evidence for the topological Anderson insulator phase, in which the band structure of an otherwise trivial wire is driven topological by the presence of added disorder. In addition, we observed the robustness of topological wires to weak disorder and measured the transition to a trivial phase in the presence of strong disorder. Atomic interactions in this quantum simulation platform will enable future realizations of strongly interacting topological fluids. △ Less

Submitted 6 February, 2018; originally announced February 2018.

Comments: 6 pages, 3 figures; 9 pages of supplementary materials

Journal ref: Science 362, 929 (2018)

A Type System for Privacy Properties (Technical Report)

Authors: Véronique Cortier, Niklas Grimm, Joseph Lallemand, Matteo Maffei

Abstract: Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy properties (e.g. ballot privacy or anonymity) is more complex and constitutes an active research topic with several recent propositions of techniques and tools. We explore a novel approach based on type systems and provide a (sou… ▽ More Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy properties (e.g. ballot privacy or anonymity) is more complex and constitutes an active research topic with several recent propositions of techniques and tools. We explore a novel approach based on type systems and provide a (sound) type system for proving equivalence of protocols, for a bounded or an unbounded number of sessions. The resulting prototype implementation has been tested on various protocols of the literature. It provides a significant speed-up (by orders of magnitude) compared to tools for a bounded number of sessions and complements in terms of expressiveness other state-of-the-art tools, such as ProVerif and Tamarin: e.g., we show that our analysis technique is the first one to handle a faithful encoding of the Helios e-voting protocol in the context of an untrusted ballot box. △ Less

Submitted 28 August, 2017; originally announced August 2017.

Topological characterization of chiral models through their long time dynamics

Authors: Maria Maffei, Alexandre Dauphin, Filippo Cardano, Maciej Lewenstein, Pietro Massignan

Abstract: We study chiral models in one spatial dimension, both static and periodically driven. We demonstrate that their topological properties may be read out through the long time limit of a bulk observable, the mean chiral displacement. The derivation of this result is done in terms of spectral projectors, allowing for a detailed understanding of the physics. We show that the proposed detection converge… ▽ More We study chiral models in one spatial dimension, both static and periodically driven. We demonstrate that their topological properties may be read out through the long time limit of a bulk observable, the mean chiral displacement. The derivation of this result is done in terms of spectral projectors, allowing for a detailed understanding of the physics. We show that the proposed detection converges rapidly and it can be implemented in a wide class of chiral systems. Furthermore, it can measure arbitrary winding numbers and topological boundaries, it applies to all non-interacting systems, independently of their quantum statistics, and it requires no additional elements, such as external fields, nor filled bands. △ Less

Submitted 22 January, 2018; v1 submitted 9 August, 2017; originally announced August 2017.

Journal ref: New J. Phys. 20, 013023 (2018)

HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving

Authors: Stefano Calzavara, Ilya Grishchenko, Matteo Maffei

Abstract: We present HornDroid, a new tool for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by an off-the-shelf SMT solver. This approach makes it possible to f… ▽ More We present HornDroid, a new tool for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by an off-the-shelf SMT solver. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still using off-the-shelf verification tools, thereby leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms state-of-the-art Android static analysis tools on benchmarks proposed by the community. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness, which covers the core of the analysis technique: besides yielding correctness assurances, this proof allowed us to identify some critical corner-cases that affect the soundness guarantees provided by some of the previous static analysis tools for Android. △ Less

Submitted 25 July, 2017; originally announced July 2017.

Comments: In Proceedings of 1st IEEE European Symposium on Security and Privacy (IEEE EuroS&P 2016)

A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications

Authors: Stefano Calzavara, Ilya Grishchenko, Adrien Koutsos, Matteo Maffei

Abstract: The present paper proposes the first static analysis for Android applications which is both flow-sensitive on the heap abstraction and provably sound with respect to a rich formal model of the Android platform. We formulate the analysis as a set of Horn clauses defining a sound over-approximation of the semantics of the Android application to analyse, borrowing ideas from recency abstraction and e… ▽ More The present paper proposes the first static analysis for Android applications which is both flow-sensitive on the heap abstraction and provably sound with respect to a rich formal model of the Android platform. We formulate the analysis as a set of Horn clauses defining a sound over-approximation of the semantics of the Android application to analyse, borrowing ideas from recency abstraction and extending them to our concurrent setting. Moreover, we implement the analysis in HornDroid, a state-of-the-art information flow analyser for Android applications. Our extension allows HornDroid to perform strong updates on heap-allocated data structures, thus significantly increasing its precision, without sacrificing its soundness guarantees. We test our implementation on DroidBench, a popular benchmark of Android applications developed by the research community, and we show that our changes to HornDroid lead to an improvement in the precision of the tool, while having only a moderate cost in terms of efficiency. Finally, we assess the scalability of our tool to the analysis of real applications. △ Less

Submitted 12 June, 2017; v1 submitted 30 May, 2017; originally announced May 2017.

A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations

Authors: Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin

Abstract: Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than develo** separate tools for special classes of effects and relational properties, we advocate using a general purpos… ▽ More Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than develo** separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and game-based cryptographic security. By relying on SMT-based automation, unary weakest preconditions, user-defined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer. △ Less

Submitted 12 October, 2019; v1 submitted 28 February, 2017; originally announced March 2017.

Comments: CPP'18 extended version with the missing ERC acknowledgement

Detection of Zak phases and topological invariants in a chiral quantum walk of twisted photons

Authors: F. Cardano, A. D'Errico, A. Dauphin, M. Maffei, B. Piccirillo, C. de Lisio, G. De Filippis, V. Cataudella, E. Santamato, L. Marrucci, M. Lewenstein, P. Massignan

Abstract: Topological insulators are fascinating states of matter exhibiting protected edge states and robust quantized features in their bulk. Here, we propose and validate experimentally a method to detect topological properties in the bulk of one-dimensional chiral systems. We first introduce the mean chiral displacement, and we show that it rapidly approaches a multiple of the Zak phase in the long time… ▽ More Topological insulators are fascinating states of matter exhibiting protected edge states and robust quantized features in their bulk. Here, we propose and validate experimentally a method to detect topological properties in the bulk of one-dimensional chiral systems. We first introduce the mean chiral displacement, and we show that it rapidly approaches a multiple of the Zak phase in the long time limit. Then we measure the Zak phase in a photonic quantum walk, by direct observation of the mean chiral displacement in its bulk. Next, we measure the Zak phase in an alternative, inequivalent timeframe, and combine the two windings to characterize the full phase diagram of this Floquet system. Finally, we prove the robustness of the measure by introducing dynamical disorder in the system. This detection method is extremely general, as it can be applied to all one-dimensional platforms simulating static or Floquet chiral systems. △ Less

Submitted 14 June, 2017; v1 submitted 20 October, 2016; originally announced October 2016.

Comments: 10 pages, 7 color figures (incl. appendices) Close to the published version

Journal ref: Nature Commun. 8, 15516 (2017)

Topological features of vector vortex beams perturbed with uniformly polarized light

Authors: Alessio D'Errico, Maria Maffei, Bruno Piccirillo, Corrado de Lisio, Filippo Cardano, Lorenzo Marrucci

Abstract: Optical singularities manifesting at the center of vector vortex beams are unstable, since their topological charge is higher than the lowest value permitted by Maxwell's equations. Inspired by conceptually similar phenomena occurring in the polarization pattern characterizing the skylight, we show how perturbations that break the symmetry of radially symmetric vector beams lead to the formation o… ▽ More Optical singularities manifesting at the center of vector vortex beams are unstable, since their topological charge is higher than the lowest value permitted by Maxwell's equations. Inspired by conceptually similar phenomena occurring in the polarization pattern characterizing the skylight, we show how perturbations that break the symmetry of radially symmetric vector beams lead to the formation of a pair of fundamental and stable singularities, i.e. points of circular polarization. We prepare a superposition of a radial (or azimuthal) vector beam and a uniformly linearly polarized Gaussian beam; by varying the amplitudes of the two fields, we control the formation of pairs of these singular points and their spatial separation. We complete this study by applying the same analysis to vector vortex beams with higher topological charges, and by investigating the features that arise when increasing the intensity of the Gaussian term. Our results can find application in the context of singularimetry, where weak fields are measured by considering them as perturbation of unstable optical beams. △ Less

Submitted 17 January, 2017; v1 submitted 18 September, 2016; originally announced September 2016.

Journal ref: Scientific Reports 7, 40195 (2017)

Dynamical moments reveal a topological quantum transition in a photonic quantum walk

Authors: Filippo Cardano, Maria Maffei, Francesco Massa, Bruno Piccirillo, Corrado de Lisio, Giulio De Filippis, Vittorio Cataudella, Enrico Santamato, Lorenzo Marrucci

Abstract: Many phenomena in solid-state physics can be understood in terms of their topological properties. Recently, controlled protocols of quantum walks are proving to be effective simulators of such phenomena. Here we report the realization of a photonic quantum walk showing both the trivial and the non-trivial topologies associated with chiral symmetry in one-dimensional periodic systems, as in the Su-… ▽ More Many phenomena in solid-state physics can be understood in terms of their topological properties. Recently, controlled protocols of quantum walks are proving to be effective simulators of such phenomena. Here we report the realization of a photonic quantum walk showing both the trivial and the non-trivial topologies associated with chiral symmetry in one-dimensional periodic systems, as in the Su-Schrieffer-Heeger model of polyacetylene. We find that the probability distribution moments of the walker position after many steps behave differently in the two topological phases and can be used as direct indicators of the quantum transition: while varying a control parameter, these moments exhibit a slope discontinuity at the transition point, and remain constant in the non-trivial phase. Extending this approach to higher dimensions, different topological classes, and other typologies of quantum phases may offer new general instruments for investigating quantum transitions in such complex systems. △ Less

Submitted 7 July, 2015; originally announced July 2015.

Journal ref: Nature Communications 7, 11439 (2016)

Hardy's paradox tested in the spin-orbit Hilbert space of single photons

Authors: Ebrahim Karimi, Filippo Cardano, Maria Maffei, Corrado de Lisio, Lorenzo Marrucci, Robert W. Boyd, Enrico Santamato

Abstract: We test experimentally the quantum ``paradox'' proposed by Lucien Hardy in 1993 [Phys. Rev. Lett. 71, 1665 (1993)] by using single photons instead of photon pairs. This is achieved by addressing two compatible degrees of freedom of the same particle, namely its spin angular momentum, determined by the photon polarization, and its orbital angular momentum, a property related to the optical transver… ▽ More We test experimentally the quantum ``paradox'' proposed by Lucien Hardy in 1993 [Phys. Rev. Lett. 71, 1665 (1993)] by using single photons instead of photon pairs. This is achieved by addressing two compatible degrees of freedom of the same particle, namely its spin angular momentum, determined by the photon polarization, and its orbital angular momentum, a property related to the optical transverse mode. Because our experiment involves a single particle, we cannot use locality to logically enforce non-contextuality, which must therefore be assumed based only on the observables' compatibility. On the other hand, our single-particle experiment can be implemented more simply and allows larger detection efficiencies than typical two-particle ones, with a potential future advantage in terms of closing the detection loopholes. △ Less

Submitted 22 March, 2014; originally announced March 2014.

Comments: 7 pages, 5 figures and 1 table

Journal ref: Physical Review A 89, 032122 (2014)