An Executable Formal Model of the VHDL in Isabelle/HOL

In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL, do not have mathematical foundation and hence are not fit for formal reasoning about the design. To enable formal reasoning in one of the most commonly used description language VHDL, we define a formal model of the VHDL language in Isabelle/HOL. Our model targets the functional part of VHDL designs used in industry, specifically the design of the LEON3 processor's integer unit. We cover a wide range of features in the VHDL language that are usually not modelled in the literature and define a novel operational semantics for it. Furthermore, our model can be exported to OCaml code for execution, turning the formal model into a VHDL simulator. We have tested our simulator against simple designs used in the literature, as well as the div32 module in the LEON3 design. The Isabelle/HOL code is publicly available: https://zhehou.github.io/apps/VHDLModel.zip

Security in Next Generation Mobile Payment Systems: A Comprehensive Survey

Cash payment is still king in several markets, accounting for more than 90\ of the payments in almost all the developing countries. The usage of mobile phones is pretty ordinary in this present era. Mobile phones have become an inseparable friend for many users, serving much more than just communication tools. Every subsequent person is heavily relying on them due to multifaceted usage and affordability. Every person wants to manage his/her daily transactions and related issues by using his/her mobile phone. With the rise and advancements of mobile-specific security, threats are evolving as well. In this paper, we provide a survey of various security models for mobile phones. We explore multiple proposed models of the mobile payment system (MPS), their technologies and comparisons, payment methods, different security mechanisms involved in MPS, and provide analysis of the encryption technologies, authentication methods, and firewall in MPS. We also present current challenges and future directions of mobile phone security.