INTEGRATING FORMAL METHODS INTO CLOUD BASED LEARNING MANAGEMENT SYSTEM SECURITY: A LIGHTWEIGHT FORMAL DEVELOPMENT FRAMEWORK

Abstract

The focus of Cloud LMS security extends beyond external protective measures, emphasizing the need for robust internal security within Cloud LMS applications, where vulnerabilities often originate. Many securities issues stem from flaws in software design, making internal security more critical than external defenses. Numerous techniques have been developed to tackle these internal security challenges, with threat modelling being a prominent approach. Threat modelling, conducted in the early stages of software development, identifies potential threats to software systems and suggests mitigation strategies. Existing methodologies, such as the Secure Development Lifecycle (SDL) and Threat Analysis Framework (TAM), often use informal or semi-formal approaches, which can introduce inconsistencies and ambiguities in system design. Formal methods, grounded in mathematics, are employed for the specification, analysis, and design of software systems, enabling precise analysis and verification at the design level. This leads to the creation of more accurate, reliable, and consistent software systems. This paper introduces a novel framework based on the lightweight application of formal methods using the STRIDE model and DREAD models, which integrates threat modelling to identify security requirements early in the development process and incorporates these security properties into the software design. The design is then analyzed, verified, and validated using formal methods including Event-B and RODIN.