Electronic health records (EHRs) play an important role in our life. However, most of the time, they are scattered and saved on different databases belonging to distinct institutions (hospitals, laboratories, clinics, etc.) geographically distributed across one or many countries. Due to this decentralization and the heterogeneity of the different involved systems, medical staff are facing difficulties in correctly collaborating by sharing, protecting, and tracking their patient’s electronic health-record history to provide them with the best care. Additionally, patients have no control over their private EHRs. Blockchain has many promising future uses for the healthcare domain because it provides a better solution for sharing data while preserving the integrity, the interoperability, the availability of the classical client–server architectures used to manage EHRS. This paper proposes a framework called HealthBlock for collaboratively sharing EHRs and their privacy preservation. Different technologies have been combined to achieve this goal. The InterPlanetary File System (IPFS) technology stores and shares patients’ EHRs in distributed off-chain storage and ensures the record’s immutability; Hyperledger Indy gives patients full control over their EHRs, and Hyperledger Fabric stores the patient-access control policy and delegations.

Most applications in the Internet such as e-banking and e-commerce use the SET and the NSL protocols to protect the communication channel between the client and the server. Then, it is crucial to ensure that these protocols respect some security properties such as confidentiality, authentication, and integrity. In this paper, we analyze the SET and the NSL protocols with respect to the confidentiality (secrecy) property. To perform this analysis, we use the interpretation functions-based method. The main idea behind the interpretation functions-based technique is to give sufficient conditions that allow to guarantee that a cryptographic protocol respects the secrecy property. The flexibility of the proposed conditions allows the verification of daily-life protocols such as SET and NSL. Also, this method could be used under different assumptions such as a variety of intruder abilities including algebraic properties of cryptographic primitives. The NSL protocol, for instance, is analyzed with and without the homomorphism property. We show also, using the SET protocol, the usefulness of this approach to correct weaknesses and problems discovered during the analysis.

Today, Android accounts for more than 80% of the global market share. Such a high rate makes Android applications an important topic that raises serious questions about its security, privacy, misbehavior and correctness. Application code analysis is obviously the most appropriate and natural means to address these issues. However, no analysis could be led with confidence in the absence of a solid formal foundation. In this paper, we propose a full-fledged formal approach to build the operational semantics of a given Android application by reverse-engineering its assembler-type code, called Smali. We call the new formal language Smali ${}^{+}$ . Its semantics consist of two parts. The first one models a single-threaded program, in which a set of main instructions is presented. The second one presents the semantics of a multi-threaded program which is an important feature in Android that has been glossed over in the-state-of-the-art works. All multi-threading essentials such as scheduling, threads communication and synchronization are considered in these semantics. The resulting semantics, forming Smali ${}^{+}$ , are intended to provide a formal basis for developing security enforcement, analysis and misbehaving detection techniques for Android applications.

The number of cybersecurity vulnerabilities keeps growing every year. Each vulnerability must be reported to the MITRE Corporation and assessed by a Counting Number Authority, which generates a metrics vector that determines its severity score. This process can take up to several weeks, with higher-severity vulnerabilities taking more time. Several authors have successfully used Deep Learning to automate the score generation process and used explainable AI to build trust with the users. However, the explanations that were shown were surface label input saliency on binary classification. This is a limitation, as several metrics are multi-class and there is much more we can achieve with XAI than just visualizing saliency. In this work, we look for actionable actions CNAs can take using XAI. We achieve state-of-the-art results using an interpretable XGBoost model, generate explanations for multi-class labels using SHAP, and use the raw Shapley values to calculate cumulative word importance and generate IF rules that allow a more transparent look at how the model classified vulnerabilities. Finally, we made the code and dataset open-source for reproducibility.