Lintent: Towards Security Type-Checking of Android Applications

Mobile devices and social media have been used to create empowering healthcare services. However, privacy and security concerns remain. Furthermore, the integration of interoperability biomedical standards is a strategic feature. Thus, the objective of this paper is to build enhanced healthcare services by merging all these components. Methodologically, the current mobile health telemonitoring architectures and their limitations are described, leading to the identification of new potentialities for a novel architecture. As a result, a standardized, secure/private, social-media-based mobile health architecture has been proposed and discussed. Additionally, a technical proof-of-concept (two Android applications) has been developed by selecting a social media (Twitter), a security envelope (open Pretty Good Privacy (openPGP)), a standard (Health Level 7 (HL7)) and an information-embedding algorithm (modifying the transparency channel, with two versions). The tests performed included a small-scale and a boundary scenario. For the former, two sizes of images were tested; for the latter, the two versions of the embedding algorithm were tested. The results show that the system is fast enough (less than 1 s) for most mHealth telemonitoring services. The architecture provides users with friendly (images shared via social media), straightforward (fast and inexpensive), secure/private and interoperable mHealth services.

Download Full-text

A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust

ACM Transactions on Programming Languages and Systems ◽

10.1145/3443420 ◽

2021 ◽

Vol 43 (1) ◽

pp. 1-73

Author(s):

David J. Pearce

Keyword(s):

Memory Management ◽

Programming Model ◽

Type System ◽

Control Flow ◽

Two Phase ◽

Type Checking ◽

Strong Focus ◽

Reference Implementation ◽

Two Phases ◽

Complex Features

Rust is a relatively new programming language that has gained significant traction since its v1.0 release in 2015. Rust aims to be a systems language that competes with C/C++. A claimed advantage of Rust is a strong focus on memory safety without garbage collection. This is primarily achieved through two concepts, namely, reference lifetimes and borrowing . Both of these are well-known ideas stemming from the literature on region-based memory management and linearity / uniqueness . Rust brings both of these ideas together to form a coherent programming model. Furthermore, Rust has a strong focus on stack-allocated data and, like C/C++ but unlike Java, permits references to local variables. Type checking in Rust can be viewed as a two-phase process: First, a traditional type checker operates in a flow-insensitive fashion; second, a borrow checker enforces an ownership invariant using a flow-sensitive analysis. In this article, we present a lightweight formalism that captures these two phases using a flow-sensitive type system that enforces “ type and borrow safety .” In particular, programs that are type and borrow safe will not attempt to dereference dangling pointers. Our calculus core captures many aspects of Rust, including copy- and move-semantics, mutable borrowing, reborrowing, partial moves, and lifetimes. In particular, it remains sufficiently lightweight to be easily digested and understood and, we argue, still captures the salient aspects of reference lifetimes and borrowing. Furthermore, extensions to the core can easily add more complex features (e.g., control-flow, tuples, method invocation). We provide a soundness proof to verify our key claims of the calculus. We also provide a reference implementation in Java with which we have model checked our calculus using over 500B input programs. We have also fuzz tested the Rust compiler using our calculus against 2B programs and, to date, found one confirmed compiler bug and several other possible issues.

Download Full-text

Making legacy Fortran code type safe through automated program transformation

The Journal of Supercomputing ◽

10.1007/s11227-021-03839-9 ◽

2021 ◽

Author(s):

Wim Vanderbauwhede

Keyword(s):

Side Effect ◽

Program Transformation ◽

The Novel ◽

Formal Approach ◽

Type Checking ◽

Type Safety ◽

Fortran Code ◽

Fortran 90 ◽

Code Type ◽

Fortran 77

AbstractFortran is still widely used in scientific computing, and a very large corpus of legacy as well as new code is written in FORTRAN 77. In general this code is not type safe, so that incorrect programs can compile without errors. In this paper, we present a formal approach to ensure type safety of legacy Fortran code through automated program transformation. The objective of this work is to reduce programming errors by guaranteeing type safety. We present the first rigorous analysis of the type safety of FORTRAN 77 and the novel program transformation and type checking algorithms required to convert FORTRAN 77 subroutines and functions into pure, side-effect free subroutines and functions in Fortran 90. We have implemented these algorithms in a source-to-source compiler which type checks and automatically transforms the legacy code. We show that the resulting code is type safe and that the pure, side-effect free and referentially transparent subroutines can readily be offloaded to accelerators.

Download Full-text