Over the past couple of years, the number of cyber-attacks and data breaches have considerably increased and so have the damages they cause, making cyber risk one of the primary concerns for top managers and world leaders around the world. Public and private organizations are therefore obliged to deploy appropriate security solutions in a bid to protect their assets against threats over time. However the complexity of information systems coupled with the interconnected nature of assets complicate efforts to identify the loopholes in an information system especially given the dynamism of cybersecurity where new vulnerabilities are discovered around the world daily. In an effort to provide IT administrators with a rapid and reliable way of detecting loopholes, the paper proposes a framework that leverages formal verification concepts to provide an abstract model of an information system with specific properties aimed at verifying the security of assets. The paper is structured as follows: section 1 introduces the article, section 2 presents some research papers related to this paper’s topic, section 3 states the problem, section 4 presents the paper’s contribution to research, and section 5 presents the proposed framework

Risk vulnerability attack surface.