IoTranx: Transactions for Safer Smart Spaces

Smart spaces such as smart homes deliver digital services to optimize space use and enhance user experience. They are composed of an Internet of Things (IoT), people, and physical content. They differ from traditional computer systems in that their cyber-physical nature ties intimately with the users and the built environment. The impact of ill-programmed applications in such spaces goes beyond loss of data or a computer crash, risking potentially physical harm to the space and its users. Ensuring smart space safety is therefore critically important to successfully deliver intimate and convenient services surrounding our daily lives. By modeling smart space as a highly dynamic database, we present IoT Transactions, an analogy to database transactions, as an abstraction for programming and executing the services as the handling of the devices in smart space. Unlike traditional database management systems that take a “clear room approach,” smart spaces take a “dirty room approach” where imperfection and unattainability of full control and guarantees are the new normal. We identify Atomicity, Isolation, Integrity and Durability (AI 2 D) as the set of properties necessary to define the safe runtime behavior for IoT transactions for maintaining “permissible device settings” of execution and to avoid or detect and resolve “impermissible settings.” Furthermore, we introduce a lock protocol, utilizing variations of lock concepts, that enforces AI 2 D safety properties during transaction processing. We show a brief proof of the protocol correctness and a detailed analytical model to evaluate its performance.

Towards an Extrinsic Formalization of Featherweight Java in Agda

Featherweight Java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as Featherweight Java. In this paper we formalize Featherweight Java, implementing the static and dynamic semantics in Agda, and proving the main safety properties for this calculus.

A Systematic Approach to Formal Analysis of QUIC Handshake Protocol Using Symbolic Model Checking

As a newly proposed secure transport protocol, QUIC aims to improve the transport performance of HTTPS traffic and enable rapid deployment and evolution of transport mechanisms. QUIC is currently in the IETF standardization process and will potentially carry a significant portion of Internet traffic in the emerging future. An important safety goal of QUIC protocol is to provide effective data service for users. To aim this safety requirement, we propose a formal analysis method to analyze the safety of QUIC handshake protocol by using model checker SPIN and cryptographic protocol verifier ProVerif. Our analysis shows the counterexamples to safety properties, which reveal a design flaw in the current protocol specification. To this end, we also propose and verify a possible fix that is able to mitigate these flaws.

Technological, functional and safety properties of lactobacilli isolates from soft wheat sourdough and their potential use as antimould cultures

Bakery products are a common medium for fungal growth due to their high-water activity and nutrients availability. The application of lactic acid bacteria (LAB) isolated from wheat bran or other cereals has shown great potential in controlling the growth of spoilage fungi, guarantee quality and prolong the shelf life of bakery products. This study outlines the antifungal, technological, functional and safety properties of autochthonous LAB microbiota isolated from type 0 soft wheat sourdough fermentation. Antifungal activity of 77 LAB belonging to Lactiplantibacillus plantarum and Lacticaseibacillus casei species isolated from spontaneous sourdough fermentation was tested in vitro against 16 spoilage fungi. Our findings demonstrated that the antifungal activity, enzymatic and safety properties of LAB isolates vary strain-dependently. Four LAB isolates (Lp. plantarum A16, A25, B11, and B15) showed the best traits, in particular strong antifungal activity and good capabilities to produce exopolysaccharides from different carbon sources in vitro. Care should be taken when using Lp. plantarum A310 and B18 and Lc. casei A23, as starter cultures, since these isolates exhibited a multiple antibiotic-resistance. Here we showed the promising potential of different LAB isolates as bio-preservative agents and to provide new insights regarding their prospective use as starter cultures to guarantee safety and palatability. Graphic abstract

PLIERS

Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: languages have high iteration costs, programmers require significant learning time, and user performance has high variance. To address these problems, we adapted both formative and summative HCI methods to make them more suitable for programming language design. We integrated these methods into a new process, PLIERS, for designing programming languages in a user-centered way. We assessed PLIERS by using it to design two new programming languages. Glacier extends Java to enable programmers to express immutability properties effectively and easily. Obsidian is a language for blockchains that includes verification of critical safety properties. Empirical studies showed that the PLIERS process resulted in languages that could be used effectively by many programmers and revealed additional opportunities for language improvement.