A formal verification framework for static analysis

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools, we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa, a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.     

FAME: A UML-based framework for modeling fuzzy self-adaptive software

Context: Software Fuzzy Self-Adaptation (SFSA) is a fuzzy control-based software self-adaptation paradigm proposed to deal with the fuzzy uncertainty existing in self-adaptive software. However, as many software engineers lack fuzzy control knowledge, it is difficult for them to design and model this kind of fuzzy self-adaptive software (F-SAS). Therefore, efficient and effective modeling technologies and tools are needed for the SFSA framework.Objective: This paper aims to identify modeling requirements of F-SAS and to provide a modeling framework to specify, design and model F-SAS systems. Such a framework can simplify modeling process of F-SAS and improve the accessibility of software engineers to the SFSA paradigm.Method: This study proposes a modeling framework called Fuzzy self-Adaptation ModEling (FAME). By extending UML, FAME creates three types of modeling views. An analysis view called Fuzzy Case Diagram is created to specify the fuzzy self-adaptation goal and the realization processes of this goal. A structure view called Fuzzy Class Diagram is created to describe the fuzzy concepts and structural characteristics of F-SAS. A behavior view called Fuzzy Sequence Diagram is created to depict the dynamic behaviors of the F-SAS systems. The framework is implemented as a plug-in of Enterprise Architect.Results: We demonstrate the effectiveness and efficiency of the proposed approach by carrying out a subject-based empirical evaluation. The results show that FAME framework can improve modeling quality of F-SAS systems by 44.38% and shorten modeling time of F-SAS systems by 38.41% in comparison with traditional UML. Thus, FAME can considerably ease the modeling process of F-SAS systems.Conclusion: FAME framework incorporates the SFSA concepts into standard UML. Therefore, it provides a direct support to model SFSA characteristics and improves the accessibility of software engineers to the SFSA paradigm. Furthermore, it behaves a good example and provides good references for modeling domain-specific software systems.     

A security evaluation framework for cloud security auditing

Cloud computing is clearly one of today’s most enticing technologies due to its scalable, flexible, and cost-efficient access to infrastructure and application services. Despite these benefits, cloud service users (CSUs) have serious concerns about the data security and privacy. Currently, there are several cloud service providers (CSPs) offering a wide range of services to their customers with varying levels of security strengths. Due to the vast diversity in the available cloud services, from the customer’s perspective, it has become difficult to decide which CSP they should use and what should be the selection criteria. Presently, there is no framework that can allow CSUs to evaluate CSPs based on their ability to meet the customer’s security requirements. We propose a framework and a mechanism that evaluate the security strength of CSPs based on the customer’s security preferences. We have shown the applicability of our security evaluation framework using a case study.     

A measurement framework for improving verification processes

This paper describes the application of quantitative techniques to software process improvement in an industrial environment. This investigation is based on theami approach which was developed during the ESPRIT II project 5494ami (Application of Metrics in Industry). The activity-based improvement paradigm behind ami (assess, analyse, metricate, improve) advocates measurement as an essential component of process improvement for understanding the process, monitoring the changes and evaluating the return on investment. This experience focuses on the improvement of reviews and inspections in a software development environment certified to ISO 9001. A measurement framework is put into place for understanding these verification processes and performing them efficiently. After a brief introduction of theami approach, the case study is described following the fourami activities. The first data analysis findings are emphasized as well as the role played by the management during the initiative.     

基于UML的商业建模及模型验证机制研究

传统的商业建模方法存在无法为商业系统开发提供一个集成的"从概念到代码"的方案的缺陷,为解决在商业建模中存在的问题,提出了使用基于UML的商业建模方法.用实例阐述了该方法的具体步骤,并针对基于UML模型形式化复杂、验证难的问题,进一步提出了一种模型形式化的方法.应用实例和实验结果表明,基于UML建模方法和形式化方法能够减少商业建模的工作量,提高商业软件的开发效率及质量,较好地解决了商业建模中存在的问题.     

A security framework for reflective Java applications

The advent of component‐based reflective applications raises the issue of protecting baselevel components from the actions performed by metalevel components. However, by their very nature, reflective applications are far more difficult to secure than non‐reflective applications, which certainly explains why the problem has received very little attention so far. In this paper we present a security framework for enforcing access control between metalevel components and the baselevel components they reflect on. Rather than designing a new security architecture from scratch, we extend the standard security architecture of Java to provide security for a fully‐functional proxy‐based MOP for Java. We implement a number of well‐known meta‐level behaviors and study their security requirements, the results of which support our design choices. Copyright © 2003 John Wiley & Sons, Ltd.     

A formal verification framework for SysML activity diagrams

SysML activity diagrams are OMG/INCOSE standard diagrams used for modeling and specifying probabilistic systems. They support systems composition by call behavior and send/receive artifacts. For verification, the existing approaches dedicated to these diagrams are limited to a restricted set of artifacts. In this paper, we propose a formal verification framework for these diagrams that supports the most important artifacts. It is based on mapping a composition of SysML activity diagrams to the input language of the probabilistic symbolic model checker called “PRISM”. To prove the soundness of our mapping approach, we capture the underlying semantics of both the SysML activity diagrams and their generated PRISM code. We found that the probabilistic equivalence relation between both semantics preserve the satisfaction of the system requirements. Finally, we demonstrate the effectiveness of our approach by presenting real case studies.     

A comprehensive framework for knowledge-base verification and validation

Before Expert System (ES) technology can be effectively used for complex systems a comprehensive verification and validation (V&V) methodology must be defined. Evidence from the computer industry suggests that without such a methodology Expert Systems will not be considered safe and reliable for field use. to this end, we have defined a design language called TOP (Terms, Operators, and Productions) for specifying knowledge-base designs which support verification and validation. This article discusses the key features of TOP which are: term subsumption, operator methods, sequence expressions, and a method for translating TOP designs into C-Language Production System (CLIPS) rules. to put these features of TOP into perspective, several illustrations from applications using TOP are presented. We believe that the concepts presented here serve as a solid foundation for practical application of Expert Systems and continued research into the verification and validation of Expert Systems. © 1994 John Wiley & Sons, Inc.     

A framework for the governance of information security

This paper highlights the importance of protecting an organization's vital business information assets by investigating several fundamental considerations that should be taken into account in this regard. Based on this, it is illustrated that information security should be a priority of executive management, including the Board and CEO and should therefore commence as a corporate governance responsibility. This paper, therefore, motivates that there is a need to integrate information security into corporate governance through the development of an information security governance (ISG) framework. This paper further proposes such a framework to aid an organization in its ISG efforts.     

A framework for automatic generation of security controller

This paper concerns the study, the development and the synthesis of mechanisms for guaranteeing the security of complex systems, i.e. systems composed of several interacting components. A complex system under analysis is described as an open system, i.e. a system in which an unspecified component (a component whose behaviour is not fixed in advance) interacts with the known part of the system. Within this formal approach, we propose techniques that aim at synthesize controller programs able to guarantee that, for all possible behaviours of the unspecified component, the system should work properly, e.g. it should be able to satisfy a certain property. For performing this task, we first need to identify the set of necessary and sufficient conditions that the unspecified component has to satisfy in order to ensure that the whole system is secure. Hence, by exploiting the satisfiability procedures for temporal logic, we automatically synthesize an appropriate controller program that forces the unspecified component to meet these conditions. This will ensure the security of the whole system. In particular, we contribute within the area of the enforcement of security properties by proposing a flexible and automated framework that goes beyond the definition of how a system should behave to work properly. Indeed, while the majority of the related work focuses on the definition of monitoring mechanisms, we also address the synthesis problem. Moreover, we describe a tool for the synthesis of secure systems which is able to generate appropriate controller programs. This tool is also able to translate the synthesized controller programs into the ConSpec language. ConSpec programs can be actually deployed for enforcing security policies on mobile Java applications by using the run‐time framework developed in the ambit of the European Project S3MS. Copyright © 2010 John Wiley & Sons, Ltd.     

A symbolic framework for multi-faceted security protocol analysis

Verification of software systems, and security protocol analysis as a particular case, requires frameworks that are expressive, so as to properly capture the relevant aspects of the system and its properties, formal, so as to be provably correct, and with a computational counterpart, so as to support the (semi-) automated certification of properties. Additionally, security protocols also present hidden assumptions about the context, specific subtleties due to the nature of the problem and sources of complexity that tend to make verification incomplete. We introduce a verification framework that is expressive enough to capture a few relevant aspects of the problem, like symmetric and asymmetric cryptography and multi-session analysis, and to make assumptions explicit, e.g., the hypotheses about the initial sharing of secret keys among honest (and malicious) participants. It features a clear separation between the modeling of the protocol functioning and the properties it is expected to enforce, the former in terms of a calculus, the latter in terms of a logic. This framework is grounded on a formal theory that allows us to prove the correctness of the verification carried out within the fully fledged model. It overcomes incompleteness by performing the analysis at a symbolic level of abstraction, which, moreover, transforms into executable verification tools.     

A security framework for cloud-based video surveillance system

Multimedia Tools and Applications - Utilizing cloud services in running large-scale video surveillance systems is not uncommon. However, special attention should be given to data security and...     

A verification approach to applied system security

We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.     

A SDR-based verification platform for 802.11 PHY layer security authentication

World Wide Web - The WiFi security authentication mechanism combined with the PHY layer information has become a hot spot of WiFi security research. The PHY layer contains rich information such as...     

A formal framework for design and verification of robotic agents

Intelligent robots are autonomous and are used in environments where human interaction is hazardous or impossible. Verification of software for intelligent robots is mandatory because in situations where intelligent robots are employed online, error recovery is almost impossible. In this paper, we provide a formal framework for offline verification of software used in robotic applications. The specification enables one to design a robotic agent which represents a class of real-life robots. Forward and inverse kinematic operations of the robotic agent are specified using the specification for rigid solids and their primitive operations. An object-oriented design of the robotic agent derived from the specifications is given. We use the specification technique VDM for our purpose.This work was partially supported by FCAR, Quebec and NSERC, Canada.     

A formal specification and verification framework for TimeWarp-based parallel simulation

The paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified, describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and type-check condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations