CAVERN
ANR-07-SESUR-003
http://www-anr-ci.cea.fr
Sécurité et Sûreté Informatique
PARTNERS
The Rule Static Analysis team in ILOG (ILOG). ILOG is amongst the worldwide leading providers of enterprise software components and associated services. Over 2,500 corporations and more than 465 leading software vendors rely on ILOG's market-leading business rule management system (BRMS), optimization and visualization software components. BRMS products account for about 40% of ILOG’s licencing and maintenance revenue. ILOG was founded in 1987 and employs more than 730 people worldwide. The company is quoted on the NASDAQ and Euronext Stock Exchanges.
ILOG has consistently built on its history of product innovation to make it the industry’s leading provider of business rule management system software. Gartner positioned ILOG in the leader’s quadrant of Gartner’s Magic Quadrant for Business Rule Engines, while Forrester Research has recognized ILOG as a rules platform market leader, including the leader in rules platforms for Java.
Since the company was founded, ILOG’s R&D department has been actively contributing to scientific and industrial research, with a strong culture of collaborating with academic and other research laboratories, in particular in the framework of collaborative research projects at the European and French level. ILOG is currently involved in the RNTL project DECIDE!, which is concerned with the application of “software model-checking”-like techniques to the analysis of rule bases.
The LIST laboratory of the CEA in Saclay (CEA) The LIST belongs to the CEA (Commissariat a I'Energie Atomique) research institute and its vocation is to help companies to increase their competitiveness through technological innovation, by transferring its technical know-how to industry. It devotes three quarters of its resources to research with partners outside the CEA. Within the List, the LSL laboratory has been conducting research and development on the Safety of Programmed Systems for over 10 years. The LSL specializes in tools for the verification and validation of software and hardware/software systems. To aid industry in the increasing automation of the verification and validation of its products, the LSL has built up, and continues to develop, an expertise in some of the most advanced techniques in the field: static analysis using Hoare logic, abstract interpretation, rewriting and proof techniques, simulation, constraint logic programming, source code instrumentation in order to collect execution data and the geometric analysis of concurrency. These techniques are implemented and used to realize different validation and verification tasks, such as: program analysis (the LSL currently participates to the RNTL CAT project (2005-2008) dedicated to the static analysis of C programs), formal proof of program properties (the CAVEAT tool [Baudin et al DSN 2002), automatic test-case generation based on the source code and/or the specifications (the PathCrawler [Williams et al. EDCC 2005] tool for automatic test-case generation for structural coverage of C programs, the GATeL [Marre ASE 2000] tool for test-case generation for LUSTRE synchronous language applications, the Osmose tool for binary level verification), automatic test-case execution by simulation, analysis of the numerical precision of calculations using floating-point numbers and proof of the properties of parallel or distributed asynchronous programs. For several years, the LSL has been investigating the use of these techniques in the security domain. It is currently involved in several projects in this domain : OpenTC, €Confidential and PFC. OpenTC (http://www.opentc.net/) is an Information Society Technologies (IST) 7th Framework Program project whose goal is to develop a secure Linux based on the Trusted Platform Module (TPM) and based on virtualisation using Xen, main partners include IBM, HP Labs, and Amd. €Confidential is an ITEA project whose goal is to ensure protection from service provider to the end user by designing security modules either on the client side of an architecture or in the network , main partners include EADS DS, Gemalto, Trusted Logic and VTT. PFC is a project of the French competitiveness cluster System@tic Paris-Region whose goal is to design and validate secure and safe embedded applications, main partners include Eads Corporate Research Center, Thales Communication, Inria.
The CeP project (which stands for ``Constraints and Proofs'') belongs to the I3S laboratory, a CNRS and university of Nice Sophia Antipolis joined research laboratory (UMR 6070). The CeP project gathers constraint programming experts and proof technique experts. The CeP project has a significant knowledge in the handling of continuous constraints whose aim is to provide a good approximation of solutions of non linear systems of constraints defined over the reals and which can not be solved using classical numerical or symbolic techniques (e.g. non linear systems of equalities and inequalities.). One contribution of the CeP project in this field is the introduction of the Quad, a global constraint which take advantage of correct linear relaxations to shrink the domain of variables over the reals. The underlying techniques involved in the Quad global constraint are quite similar to those used in the polyhedral abstract domains.
The INRIA’s LANDE project-team of IRISA (Coordinator) is concerned with formal methods for verifying and validating software. The Lande project's foundational activities are concerned with the semantics-based analysis of the behaviour of a given program. These activities draw on techniques from static and dynamic program analysis, testing and automated theorem proving. In terms of static program analysis, our foundational studies concern the specification of analyses by inference systems, the classification of analyses with respect to precision using abstract interpretation and reachability analysis for software specified as a term rewriting system. Particular analyses such as pointer analysis for C and control flow analysis for Java bytecode have been developed. For the implementation of these and other analyses, we are improving and analysing existing iterative techniques based on constraint-solving and rewriting of tree automata. Concerning the testing of software, we have in particular investigated how flow analysis of programs based on constraint solving can help in the process of generating test cases from programs and from specifications. More speculatively, a long-term goal is to integrate the techniques of abstraction and testing into a common framework for approximating program behaviour. Among the tools developed and maintained by the project, FPSE [Gotlieb Botella Watel ICSSEA 06, Botella Gotlieb Michel STVR 2006] is a symbolic evaluation tool for C programs and TAUPO [Denmat Gotlieb Ducassé 2007] is a C constraint-based verification tool. Both tools are based on the same constraint solvers library dedicated to analyze floating-point computations, C pointer manipulations and bounded integers computations. The LANDE participants to the CAVERN project are currently (only) involved in the RNTL CAT project (2005-2008) dedicated to the static analysis of C programs. As said previously, existing results of the CAT project will serve as inputs to the CAVERN project but there is no overlapping as the main theme of the CAVERN is on Constraint Programming techniques for program verification.