Commissariat &#xc0; L'&#xc9;nergie Atomique Et Aux &#xc9;nergies Alternatives

Nikolay Kosmatov

Julien Signoles

Kostyantyn Vorobyov

Mathieu Jan

Paul Dubrulle

Stéphane Louise

Christophe Gaston

Arnault Lapitre

The present invention concerns a method and a tool for designing and validating a data flow system comprising a set of software and/or hardware actors (a, a) interconnected with each other by unidirectional communication channels (c, c), the tool comprising: &#x2014;a modelling interface () configured to generate an instance of the system by specifying, in a formal manner, a real-time and reconfigurable data flow, the reconfiguration of the data flow being carried out dynamically by propagating reconfiguration data from one actor to another through the communication channels, &#x2014;an analysis module () configured to prove a predetermined set of behavioral properties of the system by means of a static analysis of the instance, &#x2014;a refinement interface () designed to allocate resources to the instance, thus establishing a configured instance, the allocation of resources being carried out in such a way that an implementation of the system complies with the configured instance, and &#x2014;a conformity test module () configured to verify the conformity of the behaviour of an implementation of the system with respect to the configured instance.

Tool and method for designing and validating a data flow system by a formal model

A method is provided that allows tracking boundaries of allocated memory blocks while still capturing byte-level properties. This is achieved with a particular shadow memory encoding scheme which captures boundaries and lengths of allocated memory blocks. Analyzing the shadow memory state allows detecting memory safety issues. In particular, for a memory location given by its address a, the proposed invention allows computing the following information: whether a has been allocated, whether a has been initialized, the start (base) address of the memory block a belongs to, the byte-length of the memory block a belongs to, the byte offset of a within its block. Such information allows for detection of specific memory safety issues at runtime.

Computer-implemented method and a system for encoding a stack application memory state using shadow memory

A computer-implemented method for encoding an application memory that a program, executed on a computer, has access to, using a shadow memory corresponding to the application memory, the method comprises: creating and initializing a shadow memory divided into segments, each segment in the application memory being mapped to a corresponding segment in the shadow memory, for each memory block in the application memory that the program allocates, encoding a corresponding shadow memory block, in the shadow memory, by: defining a meta segment preceding the first segment of the memory block in the application memory, and a corresponding shadow meta segment in the shadow memory block, writing in the shadow meta segment a first value indicative of the size of the memory block, writing, in each subsequent segment of the shadow memory block, a second value indicative of the offset between the segment and the first segment of the shadow memory block.

Computer-implemented method and a system for encoding a heap application memory state using shadow memory

Growing community of inventors

Saint-Cyr-l'Ecole, France

Nikolay Kosmatov