Preserving the confidentiality of information is a growing concern in software development. Secure information flow is intended to maintain the confidentiality of sensitive information by preventing them from flowing to attackers. This paper discusses how to ensure confidentiality for multi-threaded programs through a property called observational determinism. Operational semantics of multi-threaded programs are modeled using Kripke structures. Observational determinism is formalized in terms of divergence weak low-bisimulation. Bisimulation is an equivalence relation associating executions that simulate each other. The new property is called bisimulation-based observational determinism. Furthermore, a model checking method is proposed to verify the new property and ensure that secure information flow holds in a multi-threaded program. The model checking method successively refines the Kripke model of the program until the quotient of the model with respect to divergence weak low-bisimulation is reached. Then, bisimulation-based observational determinism is checked on the quotient, which is a minimized model of the concrete Kripke model. The time complexity of the proposed method is polynomial in the size of the Kripke model. The proposed approach has been implemented on top of PRISM, a probabilistic model checking tool. Finally, a case study is discussed to show the applicability of the proposed approach.

This paper proposes an approach to verify information flow security of concurrent programs. It discusses a hyperproperty called observational determinism which aims to ensure secure information flow in concurrent programs, and proves how this hyperproperty can be verified by stutter equivalence checking. More precisely, it defines observational determinism in terms of stutter equivalence of all traces having the same low initial value and shows how stutter trace equivalence can be verified by computing a divergence stutter bisimulation quotient. The approach is illustrated by verifying a small example.

Point-of-care (POC) analysis has emerged as a pivotal approach in providing rapid and convenient medical diagnostics. Smartphone-based solutions further augment the accessibility and ease of POC, enabling efficient on-the-go analysis. The integration of smartphone technology with POC has paved the way for innovative applications such as the Vivoo App, which empowers users to monitor various health parameters conveniently. Our study validated the accuracy and reliability of the smartphone-based POC urinalysis Vivoo mobile application. A comparative approach was followed wherein artificial urine samples were analyzed using both the Vivoo and traditional laboratory methods. A diverse range of health parameters were assessed. A total of 2618 strips were used over the course of this study to evalate the accuracy of Vivoo. The test strips results appeared to match exactly the expected measurement results. In addition, when the ±1 color block acceptance criterion was applied, 2608 of 2618 measurements of the tested strips were found to have met the expected measurement results completely. Based on the results, the 95% confidence interval for the exact match agreement proportion of Vivoo is 87.55% ± 1.27% and 99.62% ± 0.24%. As a wellness product, this study thus concludes that the Vivoo is appropriate in terms of both device reliability and performance. The app's ability to provide accurate and timely health results offers promising opportunities to improve individual health management.