Biblio

After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these components are often implemented in JavaScript, a language that is both hostile to cryptographic code and hard to reason about. So we instead target WebAssembly, a new instruction set that is supported by all major JavaScript runtimes. We present a new toolchain that compiles Low*, a low-level subset of the F* programming language, into WebAssembly. Unlike other WebAssembly compilers like Emscripten, our compilation pipeline is focused on compactness and auditability: we formalize the full translation rules in the paper and implement it in a few thousand lines of OCaml. Using this toolchain, we present two case studies. First, we build WHACL*, a WebAssembly version of the existing, verified HACL* cryptographic library. Then, we present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.

The panic among medical control, information, and device administrators is due to surmounting number of high-profile attacks on healthcare facilities. This hostile situation is going to lead the health informatics industry to cloud-hoarding of medical data, control flows, and site governance. While different healthcare enterprises opt for cloud-based solutions, it is a matter of time when fog computing environment are formed. Because of major gaps in reported techniques for fog security administration for health data i.e. absence of an overarching certification authority (CA), the security provisioning is one of the the issue that we address in this paper. We propose a security provisioning model (AZSPM) for medical devices in fog environments. We propose that the AZSPM can be build by using atomic security components that are dynamically composed. The verification of authenticity of the atomic components, for trust sake, is performed by calculating the processor clock cycles from service execution at the resident hardware platform. This verification is performed in the fully sand boxed environment. The results of the execution cycles are matched with the service specifications from the manufacturer before forwarding the mobile services to the healthcare cloud-lets. The proposed model is completely novel in the fog computing environments. We aim at building the prototype based on this model in a healthcare information system environment.