Amjad Hudaib, Ola Surakhi* and Mohammad Khanafseh
Department of Computer Science, King Abdullah II School for Information Technology, University of Jordan, Amman, Jordan
Received date: December 06, 2017; Accepted date: December 25, 2017; Published date: December 29, 2017
Citation: A Hudaib, O Surakhi, M Khanafseh (2017) A Survey on Formal Languages in the Software Development Life Cycle. Am J Compt Sci Inform Technol 5:2. doi: 10.21767/2349-3917.100011
Copyright: © 2017 Hudaib A, et al. This is an open-access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
Software; Security; Specification languages; Formal methods
Secure software is the software where unauthorized person cannot access it, modify it, or attack it. The degree of such security is measured by the existing number of security vulnerabilities. The software with no vulnerabilities is high secure software, where the software with atleast one vulnerability is insecure software.
Security in the software development is considered as a non-functional requirement that must be specified during the software development life cycle to increase the quality of the software and reduce error rate. Producing software with less error will reduce the cost and the risk which are an important factor for the stakeholder and the developers also.
Many ways can be done in order to add security to the software, some of them can be achieved by adding different activities to each phase in the development life cycle, others can be done by using specification language as a tool for checking the vulnerabilities in the software, formal methods are a mathematical based technique used for the specification, implementation, development and testing of software and hardware systems, and many more [1-14].
Second is describes different kinds of formal methods with a list for the advantages and disadvantages for each specification language and each formal method .
The rest of this paper is organize as follows; Section 2 lists some of the specification languages used for developing secure software with a comparison between them; Section 3 introduces different types of formal methods with a list for pros and cons for each one; Section 4 summarizes some of the semi-formal methods; Section 5 presents a case study and Section 6 gives the conclusion.
Software security goals
There are three principal dimensions to achieve security in the computer system, confidentiality, integrity and availability. These three aspects also are referred as CIA.
Confidentiality: means to disclose information to people or programs that are authorized to have access to that information.
Integrity: assures that a system performs its intended function in an unimpaired manner, free from deliberate or inadvertent unauthorized manipulation of the system.
Availability: assures that systems work promptly, and service is not denied to authorize users.
Availability: assures that systems work promptly, and service is not denied to authorize users.
Over the years, different security mechanism was used to achieve these goals like authentication and authorization. But the rate of attacks to computer system is increasing, and the situation may be critical especially for large systems. Because of that, many researchers pay attention on the software security field in order to produce a high secure system.
Software security basic concepts
This section will explain some of security terms that are used in this paper.
Asset: Is anything that has value to the organization, its business operations and their continuity, including information resources that support the organization's mission.
Vulnerability: A weakness in the design, operation, implementation or any process in the system which expose the system to a threat , defined it as a weakness of an asset or group of assets that can be exploited by one or more attacker.
Threat: A possible danger that may result in harm of systems and organization.
Attack: An actual event done by a person; attacker to harm as asset of the software through exploiting vulnerability.
Risk: A potential for loss, damage, or destruction of an asset as a result of a threat exploiting vulnerability.
Software security requirement: is a non-functional requirement that elicit a control, constraint, safeguard, or countermeasure to avoid or remove security vulnerabilities from requirements, design or code [17-19].
Conﬁdentiality: means to disclose information to people or programs that are authorized to have access to that information.
Integrity: assures that a system performs its intended function in an unimpaired manner, free from deliberate or inadvertent unauthorized manipulation of the system.
Availability: assures that systems work promptly, and service is not denied to authorized users.
Process: is an instance of a computer program that is being executed.
Secure software process: is a set of activities used to develop and deliver a secure software solution.
Secure software development life cycle processes
The stages of the software development are:
• Requirements definition and specification
• Design document containing system abstraction and their relationships
• Coding, Programming components of the system
• System testing
• Implementation and Maintenance
Security testing refer to the process which intended to reveal flaws in the security mechanism of an information system that protect data and maintain functionality as intended on other work security testing is making sure that all the security requirements you mapped to achieve at the beginning stages of your development of an application security program are being implemented and not just implemented but it implemented correctly.
Why security testing in SDLC is important?
Secure testing refer to one of the most important aspects on secure SDLC approach, security software testing in SDLC identifies security issue which need to be addressed, the sooner you can find them, the more money you save through fixing security issue on early stages, as bugs which will get more expensive if this security biges does not solved at early stages on software development life cycle, based on that security checking during SDLC is important , for that waiting for later stages for do security test will lead to hasty fix for security issue which discovered at this stage of development life cycle and in order to avoid the risk of discovered security issue the issue will not bode well when customer complain or worse. There are different type of security testing that can be performed throughout the life cycle will also let you know how closely the security architecture and design is being followed, In essence the security testing is a barometer of security quality within your SDLC, as well as the best way to develop and maintain applications efficiently in line with organization needs and risks, other than that the security testing important for different companies that will give the organization a strategic approach to improving security in their applications and other in business imperative.
Where does security testing fit in the SDLC
Security testing is important step for different software development life cycle, as early as during the analysis and design phases it is important to implement security testing to avoid later discovering for security issue which will cost highly expensive, security testing stages needs to be based on toy individual organization structure what the established SDLC process allows for, security testing can be broken up to three areas during the SDLC as follows:
• Security testing during analysis phase, during this phase as security requirements is mapped out, testing plans can be created to better track the completion and success of the stated requirements.
• Development phase, as soon as code is being written, static application security testing can begin, starting testing as soon as your SDLC allows facilitates, the best way to stop vulnerabilities from making their way to the finished product. With partial code scanning source code can be scanned at any point in time during the build making vulnerability discover that much faster and more effective.
• Code review testing phase, this stage become when development phase was finished and program code was built, then final security review along with manual testing can help detect logical code flaws and ensure that issues found during the development phase have been fixed correctly and new vulnerabilities have been introduced.
Four key steps for security testing in software development life cycle phases:
• Make it measurable, that mean that you can control what you can’t measure, security testing is no difference.
• 2-ensure testing tool are easy to adopt, this mean the tool which used for testing are chosen in term of learning curve and adoption rate by developers are important factors on whether or not in security testing [20-24].
• Automate wherever possible, if you are doing a good job for training your developer, you want to make sure that they are spending the most of the time doing what why were hired and trained to do, rather than instead of burdening them with long hours of code review or manual security testing at each millstone toy can automate at least parts of that process with source code analysis tools, implemented in there.
Formal specifications are a mathematical tools and techniques which can be applied to any part of software development life cycle. Basically, formal methods are applied in two phases in the SDLC, requirements and testing. The representation used in formal methods is called a formal specification language, which are based on set theory and first order predicate calculus. The language has a formal semantics that can be used to express specifications in a clear and unambiguity manner.
Formal methods facilitate the development of critical system. Previously, formal methods were used just for critical system where there is no place for error at these systems and need for testing at every stage and sub stage.
Formal methods can be classified using two ways. Firstly, according to formal specification styles, and secondly, according to software development life-cycle perspective .
Types of formal specification styles
There are different types for formal specifications methods, three main types used of formal specification style  which are described below and shown in Figure 1.
Model based specification style:
This model based specification can be used at software development life cycle as formal method which help on writing a requirement specification which used through requirement phase on SDLC, these language specify system behavior by the construction of mathematical model with an underlying state and collection of operation on that state  state model constructed with the help of mathematical entities such as relations, sets, sequences and functions and the operations of the system are specified by how can effect on the state of the system model. The most widely used notations for developing model based languages are Zed (Z) , Vienna Development Method (VDM)  and B .
Algebraic specification is a tool used to specify the system behavior by using methods derived from abstract algebra. It was originally designed for the definition of abstract data types and interface. The most widely used algebraic specification languages are: LARCH, ASL and OBJ .
This specification language used to describe concurrent system that not specified for sequential system, that this language based on specific implicate model, in these languages processes are denoted by expressions and built up by elementary expressions. Is just one language on this category, the most widely used language on process oriented specification is Communicating Sequential Process CSP .
A detailed discussion for each one of them is given as follows:
The most Model Based Languages used are:
Z: This model based language is used in requirement specification phase and verification phase of software development life cycle. It based on Zermelo-Frankel set-theory, lambda-calculus and first-order predicate logic. The specification of an application using Z- method language was done by defining the schema which is used to describe both static and dynamic aspects of a system. The Z schema consists of a name, signature part, and predicate part as shown in Figure 2. Signature past specifies attributes and the respective types of the entities. Predicate part contains the possible values that the attributes can take and specify the state and operations of a system . The Z schema consists of six main parts which are responsible on handling errors as follows: 1) the declaration of types and global variables which consists of basic types, free types, and axiomatic description. 2) The state space which presents the state variables and the relationships between them. 3) The initial state that assigns initial values to the state variables. 4) The operations which able to change the values of the state variables or remain it unchanged. 5) The error handling schemas that specify what happens if the precondition in operation schema does not hold and lastly. 6) the robust versions of operations that define the complete operations in the sense that they are able to handle errors which might occur when invalid date is input.
VDM: It is a collection of techniques for the modeling, specification and design of computer-based system. It is a model based language used in specification phase where most popular tool used on VDM is VDMTools is a rather useful tool for development of formal models in VDM++ or VDM-SL. It describes software system as a model which consists of abject and operations on the object . The objects represent input, output and internal state of the system and capture only necessary properties for expressing the essential concepts of the operation of the intended software system. MetaIV is a specification language of VDM used to express the models. The models are defined using a number of type definitions (for the objects) and function definitions (for the operations). MetaIV supports abstraction in writing specifications which is obtained through mathematical concepts, such as sets and functions. When using VDM, an abstract model traditionally contains the following components :
• Semantic domains: which describe the objects to be operated on.
• Invariants: which are the boolean functions that define a set of condition on the objects that is described by semantic domains.
• Syntactic domains: Types that define a "language" in which to express commands for manipulating the objects defined by the semantic domains.
• Well-formedness conditions: These are the functions that define when the commands, which is defined by the syntactic domains have a well-defined effect.
• Semantic functions: it provides the effect of commands on the objects defined by the semantic domains.
B: It is based on Abstract Machine notation and used for specifying, refining and implementing software . The main concept of it is to initiate with an abstract model of the system under development, a development process creates a number of proof obligations, which guarantee the correctness [25-29]. Proof obligations can then be proven by automatic or interactive prover . The most important step in the B method is proving that the algorithm in the refined machine is correct.
Different between different model based specification languages
Through this section we will do comparison between different formal specification language and choose appropriate one for particular problems, each of formal specification languages has its own property and different from other languages, for that each of these languages was suitable to be used at specific fields, through this section we will do general comparison between different formal specification languages specially languages that related to a model based specification languages as Z-notation specification language and B-method and VDM specification languages, first table (Table 1) below we will compare between different three language based on some specified factors as concurrency support and support of OOP features and other comparison factors as will show.
|Concurrency Support||Not-support concurrency control||Not-support concurrency control||Support concurrency control through VDM++|
|Support OOP Features||Support object oriented concepts such as polymorphism, inheritance and encapsulation
Using Object Z.
|No support for object oriented concept||Support object oriented concepts such as polymorphism, inheritance and encapsulation
|Basis Tool Support||Z Word
|Source code generation||Software requirement specification cannot be automatically converted into computer source code.||Software requirement specification can be automatically converted into computer source code.||Software requirement specification can be automatically converted into computer source code.|
|Security testing support||Support||Support||Support using VDM++ version|
|Phase of implementation||Z works on high level of abstraction of a system and provides a strong base for system designing and then testing it, through design phase||B models the system in an abstract machine notation that can be used further to design system, generate its code and then refine and test the same.||used to prove the equivalence of programming language concepts as part of compiler correctness arguments|
Other comparison table (Table 2) below contains comparison between different three languages based on its syntax or specification style and other feature as domain of use for each of these language, some of specification language was specified for specific domains as real-time systems and other languages was not specified for any domains or system.
|S.NO||Name of Specification language||Specification style||Domain Support|
|1||Specification language Z-notation||Sequential oriented, Property oriented and model oriented||Not Specified|
|2||Specification language B-method||Model oriented||Event B used in reactive and distributed system|
|3||Specification language VDM||Process Oriented and Model Oriented.||VDM++ used in real time and control system|
Table 2: Comparison between main three specification language based on specification style 
Other comparison can be done between this main three model based specification language based on each of these three languages paradigm and formality and other based on it executable feature for a language where Executable specifications allow using specifications as a prototype hence executable specifications save the time and significantly reducing the cost language as we will show through lower table which contain each of these language paradigm (Table 3).
|S.NO||Name Of Specification Language||Formality and Paradigm||Executable|
|1||Specification language Z-notation||Formal and state||Not executable|
|2||Specification language B-method||Formal and state||Executable|
|3||Specification language VDM||Formal and State||Not executable|
|4||Specification language VDM ++||Formal and state||Executable|
Table 3: Comparison between different specification language based on formalism and executable features
Other comparison table can be built as differentiation between different specification languages based on timing parameters as input time which used for his parameter evaluates the language on the basis of capability to handle input time. Real-time systems continuously interact with their environment and the input time is given by the environment, output time parameter which same as input time is given by the environment, output time is purely specified by the system behaviour (Table 4), the following table show how each of common specification language differentiated based on this feature as follows.
|S.NO||Name of Specification Language||Discrete continues time||Input time||Output time|
|1||Spec Lang Z||Discrete||Yes||No|
|2||Spec Lang B||Discrete||Yes||Yes|
Table 4: Differentiation of common specification language
Last comparison between different model based specification language refer to compare different languages based on its specification structure, where each of these languages has its own structure as example z specification language was defined by using a schema where it has two main part first one refer to signature part and second one is a predicate part, signature part was static or defined component and predicate part was dynamic part, as this specification language was structure other language structure was not fixed as we will show here through last comparison table between different specification languages (Table 5).
|S.NO||Name of Specification Lang||Notation|
|1.||Specification language Z-notation||Schema name
|2.||Specification language B-method||Machine name
|3.||Specification Language VDM||Type
Table 5: Comparison between different specification languages based on specification style
Algebraic specification language
There are two basic languages relating to Algebraic Specification, which are given as follows:
OBJ: It is an algebraic programming and specification language which based on algebra, first-order logic, temporal logic and set theory etc. . It is classified into two main groups:
• The one which is formed by new languages that have been designed from inception following the paradigm .
• Incorporation of object orientation into existing languages.
LARCH: The Larch family of languages supports a two-tiered, definitional style of specification, the one that is designed for a specific programming language and the other which is independent of any programming languages . The program components can communicate between each other through an interface, each interface is specified using an interface specification language. The top level of such specification is written in Larch Shared Language (LSL) which is based on first order logic with equality and induction. The second level is a Behavioural Interface Specification Language (BISL) which specifies the details of a particular implementation and defined in LSL. The basic unit of specification in LSL is a trait. A trait introduces operator names, signatures (involving type, or sort, names), and a set of axioms which define properties of the operators. Traits can be combined with other traits to structured specifications.
One language is relating to Process Oriented and described as follows:
Communicating sequential process (CSP): It is formal language for describing patterns of interaction in concurrent systems. Programs in the original CSP were written as a parallel composition of a fixed number of sequential processes communicating with each other strictly through synchronous message-passing. Each process is assigned a name and the destination name. The CSP consists of events and processes, the event is a simple action which written in a lower case, while the process consists of more than one event and written in upper case. Two main processes are SKIP and STOP. SKIP represents successful termination while STOP represents a deadlocked process which can no longer engage in any events.
Strengths and weaknesses for each of formal specification languages
After going in detail for each method of formal methods and language specified for each of formal methods, through this section we will define the strength and weakness points for each of languages used through different formal methods as given below:
Advantages: This method provides a strong base for system design and testing due to high level support on abstractions.
• Availability on market for this tool as a free tool.
• Fault can be found early on the development based on using z-method.
• Z method have a strong side which refer to behavioural specification as defining how things changes.
• Z notation used on different formal definition for testing.
• Z method presents both static and dynamic aspects of the system.
Disadvantages: This method can’t be used to generate computer source code directly.
• This method is lack of graphical notations.
• Z-method does not have any facilities for exception handling as other languages or methods
• Z-method not provides any support for concurrency control.
• Z-method formal specification does not support all aspects for of design.
• it does not contain information on how specified functionality should be achieved.
Advantages: All specification which written using VDM can be used to generate computer source code directly.
• This specification method is easy to understand
• This specification method emphasizes on concurrency control features.
• Same as Z-method it is easy to achieve this method because it is a free method.
• VDM formal specification language has facilities for exception handling rather than Z-method which not support this option.
• This method uses some function aspects of the system.
Disadvantages: This method does not support all aspect of designing of the system.
• Through this specification method some requirement can’t be specified as usability, safety, and reliability and performance requirement.
• Through VDM method the error list for all previous error can’t be emptied, based on that we can’t distinguished between new error and past errors.
• This tool has a problem which it lacks of usability and there is no internal editor for the model.
Advantages: All specification which written using b-method can be used to generate computer source code, rather than other formal specification method which not support this feature.
• Same as some other specification method b-method tool can be found as a free tool, not need to pay any fees to get this tool.
• B-method formal specification depends on abstract machine notation which it used to develop correct software.
• B-method support all software development life cycle.
• B-method support data hiding and encapsulation idea.
• B-method support automatic and interactive proof.
• B-method depends on well-understood mathematic.
• Different well-known and huge application was build based on b-method as METRO- the automatic train operating system and other system as speed control system for the SNCF and other system like smart card applications.
• B- formal specification method can be used to evaluate different dependable attributes as functionality of the system, which it refer to evaluate if the system provide the service which required by the user or not, other dependable attribute that evaluated by B-method refer to reliability of the system which refer to the probability that the software will execute without failure for a given period of time.
Disadvantages: B specification method does not support concurrency control
• B is slightly more low-level.
• This method refers to a formal method but in trough it is focused on refinement to the code rather than its original purpose.
• B specification method does not support object oriented PL
Advantages: Specification method refers to easy to use and failure with different programmers because it depends mainly on OOB features.
• This specification method fill the gap between static and dynamic specifications
• OBJ specification method support hiding and encapsulation features.
• It can be integrated smoothly with in whole development life cycles
Disadvantages: First weakness point refer to depending on object oriented programming language paradigm it give a language a powerful abstraction and structuring mechanism but this have other side effect as if we need to use a class or inheritance or objects in a true format they need to be formally defined and integrated within semantic model.
• It is difficult to integrate or to compare different approaches based on the number of interpretation and contradict unary terminology
Advantages: It is used to specify interfaces between programs in different languages.
• This formal specification method can be cop with features of different implementation languages.
• This formal specification method support the feature of abstractions
• Larch interface language encourages a style of programming that emphasizes the use of abstraction.
• Larch specification method permits specifies to make assertions about specification.
Disadvantages: Most of larch specification can’t be executed or not executable.
• This formal specification method emphasizes a simplicity and clarity rather than excitability.
• Larch specification methods do not specific or focus on all development life cycle stages especially on important stage which refer to requirement gathering stage.
In SDLC, the formal languages can be used in two phases, specification and testing. The details for each using are as follows:
Specification phase: in this phase, the system behavioral is described and its desired properties. Formal specification languages describe system properties that might include functional behavior, timing behavior, performance characteristics and internal structure, etc. . Z, VDM and Larch are used for specifying the behavior of sequential systems, while CSP focuses on specifying the behavior of concurrent systems .
Testing, verification phase: It is the process to prove or disprove the correctness of a system with respect to the formal specification or property. In order to verify the cost, two important forms can be used: Model Checking and Theorem proving .
• In model checking, a finite state model of the system is build and its state space is mechanically investigated. Two well-known and equivalent model checkers are NuSMV and SPIN.
• Mechanism of logical proof. A model of the system is described in a mathematical language and desired properties of the model can be proven by a theorem prover.
Main advantages and disadvantages of formal methods
When formal specification method used well there is a great benefits can be obtained by its use as follow:
• Through using well for formal method there is a little possibility for what has been happened was not well understood.
• Careful attention is paid to issue such as completeness and consistency for software’s which it under development, this will help to avoid overlook for certain areas which these can cause errors and bugs.
• By well use for formal method the focus will be given for what the system will do, not give attention for other details not important as how going to achieve it.
• It is possible to generate automatically programs that can do formal specification, which is more useful than do it manually, especially for large number of software’s.
Based on all upper advantages of formal method specification we can say using well for formal method can help in design flows if they are used at an early stage on SDLC phases, but if this formal method used at later stages this can helpful for determine correctness of system and weather it has been implemented properly.
The disadvantages for using formal methods are as follow:
• It is not possible to predict reliability behavior of software under developments stages, the fact that it becomes more difficult as a software get larger and more complex.
• Formal specification language depends mainly on mathematic, different participate programmer does not familier and not have enough training in the field of mathematic, this usually
• Training with formal method always deal with only toy cases or examples that have been studies previously, this suggest that most analysts do not have enough experience on complex cases because it just do training on simple cases.
• Formal methods can’t handle large and complex system development, where requirement for large and complex systems will always be problematic initially and will evolve throughout the life cycle; this creates a need for the method of requirement implementation to be flexible and robust, so that it can easily accommodate the continuous stream of change.
• Using formal method will increase the development cost especially when software is still on intial stages to do test for different requirement as do testing for security issue through different SDLC stages.
Semi-formal specification language lies between informal natural language and formal methods. It uses a graphical representation that facilitates the simulation or animation of requirements and design. Examples on the semi-formal are Entity Relationship Diagrams (ERD), Data Flow Diagrams (DFD), State Transition Diagrams (STD), Petri nets and UML (Unified Modelling Language), which will be described in detail in 4.1 sections as follows:
Entity relationship diagrams (ERD): It is a top-down graphical representation used to describe data requirements of the system. The three components of ERD are: entities, attributes and relationships.
Data flow diagrams (DFD): It is a graphical technique that depicts the flow of information and the transformations applied as information moves from input to output.
Data flow diagrams use the following symbols:
• External Entity: This represents the source or destination of a data flow. An oval containing a meaningful and unique identifier is used for this purpose.
• Process: A process is a transformation or manipulation of data flows within the system. A rectangular box that contains an identification number, a location and a descriptive title is used here.
• Data Flow: A data flow is represented by a line with an arrowhead, and is used to show the flow of information from source to destination.
• Data Store: This is a holding place for information within the system and is represented by an open ended narrow rectangle. Data store can be either long-term or short-term files, such as sales ledgers or batches of documents waiting to be processed respectively.
• Resource Flow: A resource flow shows the flow of any physical material from its source to destination. The physical material in question needs to be given a meaningful name. Resource flows are mainly restricted in early, high-level diagrams and are used when the physical low of materials is important.
DFDs are easy to learn and simple-to-understand.
State transition diagrams (STD): show the events-messagesthat trigger a transition from one state to another and the actions that result from a state change. A state represents an externally observable mode of the system’s behavior that endures for a period of time. States are connected by transitions with associated events, preconditions and consequences. A transition is the event that causes or fires a change of state.
Petri nets (PN): It is a mathematical tool used for modelling distributed systems, parallel systems modelling and analysis, communication protocols, performance evaluation and fault tolerant system.
UML: It combines a graphical notation with a semi-formal language. It has syntax and static semantics constraints need to be obeyed when models are expressed. UML supports nine diagrams:
• Use case diagrams, which is a graphic description that defines system’s user and activities and the interaction between them.
• Class diagram, which is a structural diagram for a particular system that describes classes, packages, associations and interfaces and represents a dependency of each of the classes, packages, associations or interfaces.
• Object diagrams, which are similar to Class diagram but they show single object instances and their relationships rather than classes.
• Collaboration diagrams, which show the sequence of messages sent between collaborating objects for a particular task.
• Sequence diagrams, which also show the sequence of messages sent between collaborating objects for a particular task.
• Sequence diagrams, which also show the sequence of messages sent between collaborating objects for a particular task.
• Activity diagram, which is a behavioral diagram that represent the workflow of the system. It describes the flow from one activity to another in the whole system or individually by representing one component.
• Component diagrams, illustrate the physical structure of the system in terms of its software. They show the software components and the dependencies between them
• Deployment diagrams, illustrate the physical architecture of the system in terms of the hardware it is deployed on and the communication links between hardware nodes.
Advantages and disadvantages of Semi-formal specification method
If we compare both natural languages with semi-formal methods, it can be noticed that the formal are very vague, and it is very difficult to check the completeness using informal specification method which depends on natural language based on this disadvantage or weak point for informal language, formal specification language easier than other specification language like semi-formal and informal specification method and more adoption for today application.
The disadvantages for using semi-formal specification languages can be summarized in the following point:
• Main dis-advantages of semi-formal approaches are their lack of precise semantic which can result in ambiguous interpretation of certain requirements.
• Their modelling is detailed and intuitive -they can be simple for both managers and laymen, their semantic are often imprecise, their syntax varies.
• Their syntax is varying.
In this section, we will introduce a case study to improve the security over cloud computing system specifications and reduce the number of security threats to the minimum. Two specification languages were used, UML semi-formal and Z language. The number of users in the cloud system is increasing and for large number of users, the authentication process becomes a critical issue. Using a secure system for the authentication process will help on reducing attacks and damage that may happen in the system and will reduce cost needed to recover the system after attack damage.
Having a secure requirement from the beginning of the software development will help on achieving that, the specification language can help on it. The formal language can be used for specification and testing security requirements. Here, we will use UML and Z specification languages to specify the security requirement and will introduce a comparison between them.
The security threats on the cloud system could be:
• Hacker has a login user account, or other user login information.
• Hacker makes analysis on the traffic between sender and receiver to get the login password.
The system variables are:
User: data type describes user information and contains:
• Username: user’s login name to the system.
• Password: special word chosen by the user to login the system.
• State: user’s system logging state (Online, Offline).
• Hacker tries to steal user authentication information.
• Hacker attempts to use incorrect user account.
Authentication process involves:
• User log in
• Update on the data
• Log out
The system requirements are:
• Allow user to login into the system.
• Allow user to use the system while logged in.
• Maintain user status (Login or Logout).
• Security-Alert data type contains types of alerts: a) alerts indicating malicious activities and behavior of user’s for example user try to enter invalid password, b) alert indication a successful authorized user login from specific browser or location, c) alert indicate unauthorized user, d) alert indicate using different device, e) alert indicate data modification.
System specification using UML
UML is a language used to model system behavior and structure by describing system diagrammatically and formalize user system requirements. UML models are employed for capturing interactions among the system entities, system behavior, external interfaces, system operation and other software components of the system being analyzed.
In order to build the scenario, a use case diagram shown in Figure 3 is used to describe the process as follows: the user can either register as a new user or is able to login to the system, the login system include user verification process, which will verify user information. The verification process includes three processes: the status which shows the status of the user which could be safe for the authenticated one, suspicious or blocked, update process includes the modifications that user can do if he is authorized and alert process which send alert notification if the user is not verified as described before.
System specification using Z language
Z language describes what the system does, it is an incorporation schema notation with the basic mathematical notation additionally, to help and support the structuring of specifications.
Describing the system using Z language can by using a state or model and a sequence of operations. The start of the program should be specified by an initial state, with extra predicate that defines situations of the system. The state can be change by set of operations or processes. For each process a number of predicates will identify precisely what it is required to do. Inputs and outputs may also be included. Figure 3a shows the variables of initial scenario. Figure 3b shows the first schema, LOGIN. It checks the availability of usernames and passwords in system user’s record. If unavailable, the user is blocked. If the user exists and login information is correct, then the user state changes to online, meaning the user is authentic and is signed-in to the system (Figures 3c and 3d).
This paper presents different formal specification methods and languages which can be used to construct specifications for a secure cloud computing system that is capable to limit security threats. The paper survey some of the specification languages, two kinds of specification languages were studied, the formal methods and semi-formal methods, we showed their properties, compare pros and cons for each. The results of comparison between formal and semi-formal methods showed that formal methods are stronger in behavioral specification; determine object relations and the function representation while semiformal methods are stronger in the graphical representation of the system.
All Published work is licensed under a Creative Commons Attribution 4.0 International License
Copyright © 2018 All rights reserved. iMedPub Last revised : January 23, 2018