Abstract

Abstract

Abstract

Abstract
The use of sensors in the real world is on the rise, providing information on medical diagnostics for healthcare and improving quality of life. Optical fiber sensors, as a result of their unique properties (small dimensions, capability of multiplexing, chemical inertness, and immunity to electromagnetic fields) have found wide applications, ranging from structural health monitoring to biomedical and point-of-care instrumentation. Furthermore, these sensors usually have good linearity, rapid response for real-time monitoring, and high sensitivity to external perturbations. Optical fiber sensors, thus, present several features that make them extremely attractive for a wide variety of applications, especially biomedical applications. This paper reviews achievements in the area of temperature optical fiber sensors, different configurations of the sensors reported over the last five years, and application of this technology in biomedical applications.

Abstract

Abstract
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt. © 2020 IEEE.