Stéphane Chatty

Mathieu Magnaudet

Daniel Prun

Verification of properties of interactive components from their executable code

Keywords: interactive component, verification, properties, static analysis, tree, pattern matching, specification ACM Classification H.5.2 Information Interfaces and presentation: User Interfaces, D.2.4 Software engineering: Software/Program Verification

In this paper we describe how an executable model of interactive software can be exploited to allow programmers or specifiers to express properties that will be automatically checked on the components they create or reuse. The djnn framework relies on a theoretical model of interactive software in which applications are described in their totality as hierarchies of interactive components, with no additional code. This includes high level components, but also the graphics, behaviors, computations and data manipulations that constitute them. Because of this, the structure of the application tree provides significant insights in the nature and behavior of components. Pattern recognition systems can then be used to express and check simple properties, such as the external signature of a component, its internal flows of control, or even the continued visibility of a component on a display. This provides programmers with solutions for checking their components, ensuring non-regression, or working in a contract-oriented fashion with other UI development stakeholders.

INTRODUCTION

Using executable representations of programs to verify software properties by static analysis is a well established technique. Static analysis requires no additional modeling work from developers, and can be performed automatically on the source code or on intermediate representations produced during its compilation. With languages such as Java and C it has become a standard step in development processes: programmers rely on the compiler to detect unused arguments, incompatible types, and unusual control flows. Static analysis is also what gives domain specific languages, such as SCADE for command and control systems and VHDL for hardware circuits, a key role in the development of critical systems for fields such as transportation, health and defense.

Static analysis has even been used with languages like Eiffel to introduce software engineering methods based on contracts. Instead of checking generic properties only, the compiler checks properties defined by development teams for individual components. This helps them to organize developments and ensure non-regression.

However, there are limitations to applying these methods to human-centered software such as surveillance systems and vehicle cockpits. Interactive software is software that interacts with its environment, which may include users, pervasive sensors and control systems. This brings additional desired properties, related to how the software will interact. For instance, when working on a graphical button one may want to guarantee that the button will always have three visually different states, and not only that its code will not crash. But various categories of interactive software, including modern user interfaces, have part of their code written with traditional programming languages. This makes the verification of interaction-oriented properties difficult because the native code may have an influence on these properties but it is not accessible to analysis at the desired level of abstraction. In practice, development teams must generally do with traditional computation-oriented verifications.

In this article we present verifications of interaction-oriented properties that are made possible by using an executable language dedicated to interactive software. After reviewing the state of the art we present the djnn programming framework that executes descriptions of interactive components, and show how these descriptions are organized like an abstract syntax tree. We then show how properties can be statically derived from this tree with pattern matching techniques such as XPath. We conclude on the perspectives in terms of methods and tools for developing interactive systems.

STATE OF THE ART

Properties of interactive systems

As stated in [START_REF] Abowd | Structuring the space of interactive system properties[END_REF], an interactive property is a feature of an interactive system that is the subject of analysis and evaluation. During the system definition phase, interactive properties are used to express user needs without any consideration about how they will be fulfilled. They allow external stakeholders of the system (for example the final user) to capture all features expected from the future system. Properties are also used as drivers for the design: they define the limits in the design space in which the solution must fit. Finally, they are used as a reference for the validation phase during which the final system is checked against the user needs. Such properties are often expressed at task level: "when activated, the alarm must always be visible by the user"; "the user must always have the possibility to abort a task".

Another way to use properties has been pointed out in [START_REF] Campos | The role of verification in interactive systems design[END_REF], properties are defined during the iterative design of interactive software and used to support and justify design choices. Directly aimed at designers' concerns, properties address technical features resulting from design elements (input devices, displays, etc) and design choices (interaction style). Examples of such properties are "all mouse press on one graphical component have an effect on another component" and "the resolution of the printer is 9600 dpi".

In parallel a lot of effort has been spent on classifying interaction-oriented properties. Works initially done in [START_REF] Mccall | Factors in Software Quality: Preliminary Handbook on Software Quality for an Acquisiton Manager[END_REF], [START_REF] Cavano | A framework for the measurement of software quality[END_REF] and in software standards have defined several criteria to assess whether a final product meets its expected goals. Criteria focused on usability (learnability, flexibility, robustness) have been added later for graphical user interfaces [START_REF] Abowd | Structuring the space of interactive system properties[END_REF], then multimodal user interfaces [START_REF] Nigay | Multifeature Systems: The CARE Properties and Their Impact on Software Design[END_REF]. In accordance with [START_REF] Campos | The role of verification in interactive systems design[END_REF], these works showed how interaction can be correlated with relationships between design level properties (related to devices, interaction, language) and system level (tasks).

Verification of interactive system properties

During the last decades, several methods for the verification of interactive system properties have been proposed. The empirical method relies on the execution of the final system (or a prototype) with end-users accomplishing selected tasks, in a dedicated environment. During the execution, measurements and observations are performed. Collected data are then used to assess whether the system fulfills the expected properties or not. This approach is widely used for interactive system evaluation and for many properties it is the only available method. The main drawback is its lack of exhaustivity, because properties cannot be checked against all possible executions of the system. This is compounded by the cost of empirical tests, which limits the number of tests that can be run.

Another approach consists of using model-based methods: during the design, a model of the future system is built and properties are verified on the model rather than on the final system itself. The underlying logic behind this approach is that if a property holds on the model, and if the final system is built according to the model, then the property holds on the final system. Several kinds of models can be used according to the nature of the system and the properties to be checked. Formal models are models whose syntax and semantics are defined in an unambiguous way. This allows to define proven model transformations and analysis algorithms that can be used for verifying properties. For example, dedicated algorithms on Petri net models can identify loops within the control flow or prove ressource boundedness; refinement proofs on B models can show that an invariant is preserved when adding more details to a model.

Model checking methods are a class of model-based methods.

They are based on the evaluation of logical properties on the state-transition structure obtained from the simulation of the model. For instance a combination of the LOTOS language and the task model Concur Task Tree has been proposed to verify dynamic properties of the user interface [START_REF] Paternò | Formal reasoning about dialogue properties with automatic support[END_REF]. Interactive Cooperative Objects follow a similar approach, using Petri nets to model part of the behavior of interactive components [START_REF] Palanque | A model-based approach for supporting engineering usability evaluation of interaction techniques[END_REF]. Safety properties of synchronous languages Lustre and Esterel are also checked with model checking [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF][START_REF] Berry | ESTEREL: A formal method applied to avionic software development[END_REF].

Alternatively, proof-based methods are a class of modelbased methods where the model is described by a set of variables, operations, events, temporal properties and invariants. The operations must preserve these invariants and a set of other properties (preconditions and/or post conditions). To ensure the correctness of these specifications a set of proofs is generated and shall be proved. In the field of interactive software, VDM [START_REF] Duke | Abstract interaction objects[END_REF] and Z [START_REF] Hussey | Specifying a Web Browser Interface Using Object-Z[END_REF] have been used for defining atomic structures like interactors. The B language has been used to express the design of a system by the way of successive refinements starting from task model level to code level [START_REF] Aït Ameur | Encoding a process algebra using the Event B method[END_REF]. Finally, logics and type systems have been also applied. HOL (a higher order logic theorem prover) has been used in the verification of user interface specifications [START_REF] Bumbulis | Validating properties of component-based graphical user interfaces[END_REF].

In the context of interactive systems, models are mainly used to express elements with a high level of abstraction. For example many models describe information related to Abstract User Interfaces (AUI). A lot of details related to the concrete interface, including the description of modalities, are not or little included in the models, which makes hard or even excludes the verification of some properties.

Abstract interpretation of software

Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] consists in giving an abstract semantics to a programming or specification language so as to perform operations on the abstract representation: property verification, optimisation, debugging. Concrete semantics are mathematically well defined objects that explicit the meaning and the possible behaviors of the program. Concrete semantics are generally not computable, which makes all non-trivial properties undecidable. To avoid this, abstract semantics are introduced as computable approximations of concrete semantics in which more properties are decidable. Static analysis is the major concrete application of abstract interpretation. It is applied by analyzing the source code of programs and automatically extracting an abstract semantic that can be used to verify properties and perform optimisations. This approach has been used in software compilers for a long time (for example [START_REF] Pop | The SSA Representation Framework: Semantics, Analyses and GCC Implementation[END_REF] uses it for the optimisation of the gcc compiler, [START_REF] Burke | Interprocedural dependence analysis and parallelization[END_REF], [START_REF] Kennedy | Optimizing Compilers for Modern Architectures: A Dependence-based Approach[END_REF] and [START_REF] Lim | Maximizing parallelism and minimizing synchronization with affine transforms[END_REF] for automatic software parallelisation). This approach has also been used for the verification of various properties of programs: the static analyzer Astrée is able to prove the absence of some types of run time errors on C programs [START_REF] Blanchet | Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software[END_REF], and has been used in safety-critical projects. The FLUCTUAT tool [START_REF] Goubault | Asserting the precision of floating-point computations: A simple abstract interpreter[END_REF] is an abstract interpreta-tion tool for studying numerical C programs, and in particular the propagation of uncertainties in floating-point computations.

There have been some works on using abstract interpretation for interactive properties. [START_REF] Charlier | Abstract interpretation and application to interactive system verification[END_REF] first advocated this approach with the objective of providing a unification canvas for verification techniques. [START_REF] González-Calleros | Advanced human-machine interface automatic evaluation[END_REF] described the verification of interactive Web pages through the static analysis of the user interface and ergonomic rules, encoded in UsiXML. [START_REF] Thimbleby | Applying graph theory to interaction design[END_REF] proposed to exploit a graph-oriented semantics of an interactive device to support the verification of properties. In this work, an existing device was analyzed and modeled with a graph whose arcs represent user actions and nodes observable states. It was then possible to compute some interactive properties on the graph that can be interpreted at the device level. Despite its success, this work illustrates the constraints that often apply to using abstract interpretation on interactive systems: when the system is built with tools that do not capture the appropriate level of information, the missing information must be introduced by producing a model by hand.

In order to support fully automated verifications, one must ensure that what programmers or designers produce contain all the necessary information to derive an abstract interpretation. Any part of the software built with a traditional language foils this approach, because it would be extremely difficult to reconstruct the impact of this piece of code on the program's interactive behavior automatically. Model-based engineering solves this by having humans create task descriptions and deriving the code from this. An alternative consists in providing programmers with an interaction-oriented language that allows them to describe complete applications at an appropriate level of abstraction.

THE DJNN FRAMEWORK

djnn is a programming framework that relies on a model of interactive software in which any program can be described as a tree of interactive components [START_REF] Chatty | Supporting multidisciplinary software composition for interactive applications[END_REF]. Basic components such as variables, control structures, and graphical objects are assembled to produce bigger components, themselves assembled until producing the desired application.

The execution of a program is described by the interactions between its components, and between them and the external environment: components react to events detected in their environment, and may themselves trigger events. For instance, a simple "hello world" program can be described with two components. The first prints text when activated, and the second binds the activation of the first to the start of the program. Launching the program is an external event that triggers the start of the program, thus triggering the binding component which itself triggers the text-printing component. djnn has the expressive potential of a general programming language. This contrasts with most user interface programming frameworks, which provide reusable components and architecture patterns that programmers combine with code written in a traditional programming language. Not only does djnn aim at covering 100% of the user interface code, it also has the potential of describing the functional core as well, thus covering whole interactive applications.

Creating a program as a hierarchy of components is similar to constructing an abstract syntax tree, as done by traditional compilers. The tree contains all the information needed to execute the program directly or translate it into executable code for a given platform. It also lends itself to static analysis, because all the components of the tree can be interpreted in a common semantic framework. This is what we propose to exploit in the rest of this paper, after giving more details on djnn and its component system.

Root concepts: processes

The conceptual model of djnn can be compared to that of functional programming languages: it relies on a very reduced set of concepts, from which all other language concepts and programmer-defined concepts are derived. In functional languages the basic concepts are functions, arguments and function calls, all rooted in the theoretical concept of lambda term from lambda calculus. In djnn the basic concepts are components, names and activation, all rooted in the theoretical concept of process from process algebras [START_REF] Baeten | A brief history of process algebra[END_REF].

Like computations can be described as the evaluation of lambda expressions, interactions can be described as the activation of interconnected processes: activation signals, called events, propagate from one process to another according to how they are coupled, thus producing the reactive behavior of the system. Process-based theories are general enough to model both interaction-oriented software and computationoriented software [START_REF] Goldin | Interactive computation -the new paradigm[END_REF]. But they can also model hardware devices, and more generally the environment in which software applications run. This allows to model both the software and its direct environment using processes, so that no special provision has to be made for those part of the software that interact with the environment. Whole interactive applications can therefore be described in the same language.

Interactive components

Component are man-made embodiment of processes: engineers build systems by assembling components, and the theoretical model of the resulting systems can be deduced from those of the individual components and how they are assembled. This includes hardware components as well as software, programmers being in charge of the latter. Programmers create interactive programs by instantiating and assembling software components, and connecting them to hardware components. The djnn environment provides them with basic software components to this effect:

• components that support user interaction, either because they are software proxies for hardware devices (e.g. mouse, display monitor) as in [START_REF] Chatty | Multiple input support in a model-based interaction framework[END_REF] or they represent abstractions created on top of hardware devices (e.g. graphical objects, windows, sounds, speech grammar rules);

• components for data representation, such as numerical, text and boolean values;

• computation-oriented components, such as numerical, geometrical and logical operators;

• components that encapsulate pre-existing code written in another language, such as gesture recognition algorithms;

• components aimed at assembling and connecting other components; this includes composite components for grouping, and control structures for connecting components to ensure that they will interact.

Like in traditional software, control structures are the key to providing programmers with the appropriate power of expression. djnn provides the control structures that have been introduced for interactive software in the last decades, as well as traditional computation-oriented control structures. This includes:

• bindings, which ensure simple reactions to events: when two components are interconnected by a binding, activation of the first triggers activation of the second;

• connectors, which ensure that any modification of their input value are propagated to their output values;

• state machines, whose transitions can be triggered by the activation of components, and whose states and transitions can trigger the activation of other components;

• composite components, which propagate their activation to their sub-components;

• iterators, which activate other components in a given order;

• tests, which activate another component only when they are activated and when a boolean value is true;

• switches, which activate one among several components depending on the value of their state.

Programmers can extend this basic set by assembling available components to produce new control structures dedicated to their own needs, for instance control structures dedicated to software adaptation as suggested in [START_REF] Magnaudet | What should adaptivity mean to interactive software programmers?[END_REF].

Component hierarchies

Even though programs can be described in their totality by interconnected components, programmers need additional services to manage their code. To start with, when using textbased languages they need to use names to designate the components they wish to interconnect. These names are not essential to program execution and can disappear during compilation, nevertheless they are essential to writing programs. Similarly, programmers need means to organize their components so as to understand how their programs work, organize their tasks, and reuse components between programs.

The composite components of djnn provide support for both organizing components and naming them. Because they contain other components, they allow to create component hierarchies. For instance, a text is part of a button, itself part of a dialogue box, and so on. This defines a natural scheme for naming components: if each component has a name relative to its parent, all components become addressable with names such as mydialogue/ok/label. In this example, the clock, increment, multiplier, binding, connector, circle, rotation and needle are basic components provided by djnn. The control component represents the underlying mechanics in the wall clock. Every 1000 milliseconds, the clock named cl is activated. Because this clock is bound to the increment named incr by an anonymous binding, the state of the increment increases by one each time. Since we want the needle to turn by 6 degrees, the state of the increment is fed through an anonymous connector to the left input of the multiplier named mult, and the right input of the multiplier is set to 6. Consequently, the result of the multiplier increases by steps of 6 every 1000 milliseconds. The graphics component is a small graphical scene made of a circle, a rotation and a line. Because of its position in the order of the scene, the line is drawn on top of the circle and is rotated by the amount defined in the rotation component. Consequently, the effect of the last anonymous connector is to ensure that the needle is rotated by 6 degrees every second.

Semantics of the hierarchy

The names used in the connectors of the above example, e.g. control/mult/result, are representative of how the hierarchy of components is used. This hierarchical structure allows programmers to think of their applications as trees of components, to address components as tree branches, and to reuse whole branches as components in other applications. It also provides the basis for drawing a parallel between the djnn component hierarchy and the abstract syntax trees of traditional languages. In both cases, the execution of the program is defined by a graph of interconnected elements. This graph contains elements that can point at any other element: for instance a function can call itself recursively and a button can trigger the closing of its parent dialogue box, thus creating a loop in the graph. But in both cases, a tree-like subset of this graph captures how the program was organized by programmers. This dual structure is exploited by compilers and by static analysis tools for computation-oriented software. Similarly, we can exploit it to verify interaction properties of djnn components.

With djnn the significance of the tree structure is even higher than usual because, like with XML-based formats such as SVG and HTML and unlike with traditional programming languages, the structure of djnn programs is the same as the structure of their data. This is because interactive applications, and particularly graphical applications, generally have a static structure in which data and behavior are intermixed. For instance, a dialog box is made of a basis of graphics, to which behavior was added. This combination of data and behavior is so meaningful to programmers and designers that it guided the design of user interface programming tools, including djnn and its component model. At the opposite, computation-oriented programs have a syntactic structure that is guided by software reuse and not by any data structure. This central role of the tree means that important properties can be evaluated by analyzing it, without need to explore the full graph. In particular, since the introduction of graphical "scene graphs" decades ago the tree structure of interactive applications has been used to express execution control. The position of a graphical object in the tree does not only tell to which component it belongs, it also tells its relative position to other graphical objects in the same component. Thus, a component situated on the right of another one in the tree will be displayed on top of it if their coordinates overlap. In the same way, djnn implements a flavor of graphical scene graphs in which graphical style components such as color, opacity and stroke width can be placed in the tree and act as context modifiers that affect all the shapes that follow. The shapes added to the right of these style components are then affected by them (see Figure 1). This also applies to geometrical transformations (rotation, scale, translation). The djnn hierarchy of components is an augmented scene graph that contains components as varied as control structures, sounds, files and numerical operators, and sometimes even does not contain graphical objects at all. For consistency, the original context-oriented semantics of the order of components in the tree was maintained and used for other modalities when this is meaningful. This can be easily exploited toward the verification of properties. For instance, as detailed later, it makes it possible to answer questions such as "will this component be overlaid by another one?", "is the color difference between the background and the foreground components large enough?", "is the display of this message triggered by the right sensor?" or "is there an event source connected to each transition of the finite state machine?".

Building and exploring the component hierarchy

djnn can be used as a traditional toolkit in which all components are created through a C, C++, Perl, Python or Java API. For instance, the following Java code creates the wall clock described earlier.

wallclock = new Component("wallclock"); control = new Component(wallclock, "control"); cl = new Clock(control, "cl", 1000); incr = new Incr(control, "incr", 1); new Multiplier(control, "mult", 0, 6); new Connector(control, 0, incr, "state", mult, "left"); new Binding(control, 0, cl, 0, inc, 0); graphics = new Component(wallclock, "graphics"); new Circle (graphics, "bkg", 250, 250, 100); new Rotation(graphics, "r", 0, 250, 250); new Line(graphics, "seconds", 250, 250, 250, 150); new Connector(wallclock, 0, control, "mult/result", graphics, "r/angle");

But, as illustrated in Figure 2, djnn can also be used as an interpreter for components that are produced with external tools, and all or parts of djnn programs can be loaded from XML files and executed by the djnn interpreter. For instance, the above wallclock can be executed from the following file:

<component name="wallclock"> <component name="control"> <clock name="cl" period="1000"/> <incr name="incr"/> <multiplier name="mult" left="0" right="6"/> <connector in="incr/state" out="mult/left"/> <binding source="cl" action="incr"/> </component> <component name="graphics"> <circle name="bkg" cx="250" cy="250" r="100"/> <rotation name="r" cx="250" cy="250" a="0"/> <line name="sec" x1="250" y1="250" x2="250" y2="150"/> </component> <connector in="control/mult/result" out="graphics/r/a"/> </component>

The djnn interpreter can be compared to a Java virtual machine, and the djnn XML format to Java byte code. In both cases, executable programs are loaded in memory and run by an interpreter. In this context, the traditional toolkit API of djnn can be considered as an alternative byte code format: components are either stored in XML or in compiled code. This architecture that separates an interpreter and an executable set of components provides two solutions for performing static analysis of the components. The hierarchy of components can be analyzed in memory, whatever method was used for creating it. This can be done by adding analysis tools to the djnn interpreter. Alternatively, analyses can be performed on XML files using dedicated analytical tools.

ANALYZING DJNN COMPONENTS

As stated previously, the hierarchy of components in djnn carries a significant part of the semantics of a djnn program. Consequently, a number of properties can be checked by analysing the tree of components. In this section, we describe several kinds of such analyses. We start with some properties that can be verified by pattern matching in the tree only. For practical reasons, we use XPath queries, although other methods may prove useful in the future. We then move to properties that need additional more sophisticated graph analysis.

Pattern matching with XPath

XPath is a language specified by the WWW Consortium [START_REF] Gulliksen | XML path language (XPath) 2.0[END_REF], originally dedicated to the exploration of XML trees. It defines a rich grammar to build expressions that can be used to select nodes in a hierarchical document. The syntax of an XPath expression can be quite complex. It offers various constructs to specify a search path (relative, absolute), to express relationships, called axes, between the nodes (parent, children, sibling, descendant, etc.) and to check properties of the elements or their attributes through logical and arithmetic expressions. Processing an XPath query results in a list of items that all contain elements that match the expression. For example the expression expr=(/widget/descendant:: * /button) retrieves all the "button" elements that descend from the "widget" element.

Although XPath was designed for XML, it can be used with any hierarchical structure that is similar enough to the ontology of an XML document: element, element value, attribute, attribute value, etc. This is the case of the hierarchies of components in djnn, both in their XML form and when loaded in the djnn interpreter. When executing a djnn program, two phases can be distinguished: the building of the hierarchy of components in memory, then its execution. We focus on the first phase, in which djnn can perform static analysis automatically before running the program. This provides a convenient time, if not always optimal, to provide developers with feedback on the robustness of their code.

Verifying component signature

Most modern developments involve teams of developers that build or evolve components in parallel then combine them. In the case of graphical user interfaces, this concurrent engineering can even involve different professions, with graphical designers producing the visual components and programmers producing the rest. The efficiency of this development process would be improved if all developers could verify before integration that their components follow the contract that was originally decided upon. Here, a number of such contracts can be defined as the existence of a specific pattern of descendants in a component.

Suppose for example that one creates a new widget for a WIMP toolkit. It must then be checked that this widget has a width and a height children to ensure that it will be possible to connect them to the layout system. Such a verification can be made by checking that the XPath expressions expr=(/widget/width) and expr=(/widget/height) do not return a null result.

Similarly, before adding a drag and drop behavior to a component, we must check the existence of the press/x and press/y patterns, that is the event and properties that will trigger the behavior, as well as the existence of and x and y children, that is the properties that will be changed by the behavior. The corresponding XPath requests are, respectively, expr=(/component/press/x), expr=(/component/press/y), expr=(/component/x) and expr=(/component/y).

Patterns can also be used in a more flexible way. Suppose that one wants to build a clock with three needles for hours, minutes and seconds. Coding the clock behavior involves triggering a periodical change of the angle of the needles around their respective rotation center. This code can only work if the graphics have three needles. A good way to verify this condition is to check it through an XPath request: the graphical component must contain components called hours, minutes and seconds. XPath allows to find a component without assuming any specific place for it in the tree. For instance, the expression expr=(//hours) will find, if it exists, the hours component whatever its position in the graphical component. Note that the condition is verified for many different graphical design (e.g. figure 3). Thus, this verification focuses on what is needed exactly and does not impose a strong restriction over the power of expression.

Verifying execution context

The specification of an interactive system sometimes includes the expression of constraints on the hardware and software environment in which a given application will run. For instance, some applications require a minimum screen size to ensure readability and others require a specific input device to support a specific interaction style. Some of these constraints can be checked through XPath requests over the extended djnn tree, that includes the context.

The djnn framework gives programmers the possibility to explore an extended component hierarchy that represents the context in which their program runs. Their own components, when created, become part of this extended tree. Upon request, the extended tree can contain the available physical displays, the input devices, the batteries, etc. Once initialized, the extended tree can be explored like the application tree and its components can be used in control structures in the application tree. Consequently, verifying that a large enough physical display is available amounts to verifying the existence of a specific component in the display tree through an XPath request such as: (/displays/display[@width > 800]). Figure 4 shows how the result of the query can be used to decide whether or not to launch a program depending on the current hardware configuration.

Verifying component visibility

As mentioned earlier, the order of graphical components in tree determines what will effectively be displayed. Based on this, it becomes possible to verify some properties such as the visibility of a graphical component. The properties to be verified are, at least, that the component is rightmost in the tree and that there is no opacity components with a zero value on its left. Moreover we have to check that, if an opacity component is present in the context, there is no event source that can modify it. The following example illustrates such a situation: <component uri="djnn://root"> <clock name="cl" period="100"/> <incr name="incr" /> <formula name="f" formula="a = (1-i/100)"/> <connector in="djnn://root/incr/state" out="djnn://root/f/i"/> <binding name="b" source="djnn://root/cl" action="djnn://root/incr"/> <frame name="frame" title="myFrame" x="50" y="50" width="250.00" height="250.00"/> <fill-color name="fc" r="30" g="10" b="200"/> <fill-opacity name="fo" a="0.81"/> <connector in="djnn://root/f/_child3/result" out="djnn://root/fo/a"/> <rectangle name="myR" x="10" y="10" width="150" height="100" rx="0.5" ry="0.5"/> </component> This piece of XML is a complete representation of a simple program. The program displays a blue rectangle, and a clock periodically triggers an increment that is used through a calculation to modify a fill-opacity component (Figure 5). We want to check if the rectangle is always visible.

It is quite easy to see, on this example, that the rectangle is the last graphical shape of the tree. We can also automate this verification, by combining XPath queries in a simple algorithm. Firstly, we have to check the very existence of the graphical object of interest. If the object's name is top then we can check that the expression exp = (/descendant:: * [@name='top']) does not return a null result. Then we have to verify that no graphical shape can mask it. The method consists in retrieving the list of all the graphical shapes situated in the tree after the closing tag of the top component. This list can be retrieved with a series of XPath expressions of the form:

/descendant:: * [@name='top']/following:: * /rectangle where the last name is replaced by the different kinds of graphical shapes (rectangle, circle, path, etc.). For each expression, it must be verified that the returned list is empty.

The second step consists in checking that there is no opacity component at the left of the component. Similarly, with the expression:

/descendant:: * [@name='top']/preceding:: * /fill-opacity it is possible to verify if there is an opacity component that can change the visibility of the component top. Of course, the opacity value can be high enough to guarantee the visibility of the following components. But we have to detect if the value can be changed during execution. Opacity components have a property named a whose value fixes the current opacity. Thus, if the name of the opacity component is fo, then we have to check if there is a data flow component, a connector, whose output value ends with fo/a. Once again we can build an XPath expression to retrieve all the connectors of the tree: /descendant:: * /connector Then, with a simple algorithm, it is possible for each node to retrieve the value of its output attribute and to verify whether or not it ends with the specified suffix. If this is the case, this means that the property can change during execution, and that the visibility of the component cannot be ensured.

Verifying the control flow

The combination of XPath queries to select elements and simple algorithms over their results allows to address more complex cases. The example shown in Figure 6 is a classic cockpit component, the primary flight display, here represented with an alarm message on the top. This message alert must be triggered by a proximity sensor that has two children true and false. The message must be displayed when the true child of the sensor is active and must disappear when the false child is active. The usual way offered by djnn to program this behavior is to combine a switch component and a finite state machine (FSM). Any number of children can be added to a switch but only one is active at a given time; which child is active is defined by the state of the switch. When the state of a FSM is connected to the state of the switch, the FSM controls which child is active. In our case, adding the alarm message to one branch of a switch ensures that it is visible when the FSM decides that this branch is active. This ensures that the visibility of the message is controlled by events received by the FSM.

Consequently, to verify the behavior of the alarm we have to check at least that:

1. the alarm message component is a child of a switch; 2. the switch is connected to a FSM; 3. the FSM is well formed; 4. there is a bijection between the branches of the switch and the states of the FSM;

5. the transition in the FSM that goes to the alarm state is triggered by the right event source.

Regarding point 1, the parent of an element can be easily retrieved through the following XPath expression: expr = //descendant:: * /component[@name='terrain_alert']/parent::node()

Once found, we can check that it is actually a switch through the attribute name of the node. For point 2, we have to verify the existence of a connector that connects a FSM to the switch found previously. This can be done by chaining XPath requests. The first finds all the elements in the tree whose node type is connector. Then we can look for a connector whose in attribute corresponds to the state of a fsm node and out to the state of the switch. If a connected FSM is found, we can make classic verifications on it (point 3) such as "is there a transition allowing to reach each state?". This means here: S = XPath.evaluate ("/fsm/children:: * /state") T = XPath.evaluate ("/fsm/children:: * /transition") for each state s in S verify that: exists t in T such that output (t) = s

We also have to check that for each branch of the switch, there is a corresponding state in the connected FSM (point 4).

For this, we must verify that for each branch of the switch, it exists a state in the FSM with the same name. Finally, to verify point 5 we have to follow the control flow that goes from the transition whose output is the alert state, to the event source that will ultimately triggers it. This step can be seen as a partial traversal of the control flow graph. It consists in collecting the control nodes of the tree and in exploring the input and output nodes that they connect.

We implemented the final verification as a Java test that runs the XPath queries on the XML version of the program, then executes the above steps. In our program, there is a connector c1 between the switch controlling the message and a FSM. The transitions of the FSM are connected to the terrain alert and end terrain alert components, themselves connected to the true and false children of the proximity sensor through two bindings components b1 and b2.

The result is the following: Thus we can verify that the alert message will indeed be displayed only when the true child of the proximity sensor is activated.

PRACTICAL APPLICATIONS AND PERSPECTIVES

djnn is available at http://djnn.net. It was designed to support the development of modern interactive systems, including post-WIMP and multimodal interaction, ubiquitous computing and internet of things applications, and to explore new engineering processes for interactive software. Since practical application to real life developments is essential to the validation of the underlying research, djnn is maintained and proposed to user interface developers on several operating systems. It comes with a complete graphical module, and with partial support for modern input devices, multiple displays and file management. Other modules are under development for supporting various interaction modalities, all based on the theoretical principles explained earlier and thus all accessible to static analysis.

djnn has been used to develop various real-size applications including a touch-based ground control station for squads of drones, a pen-based map annotation system for crews of search and rescue missions, a multimodal cockpit prototype for civil aircraft, and an interactive show room. Some are illustrated in the djnn web site. All these applications have been designed and implemented using the same process: user-centered design methods yielding low fidelity prototypes (mostly paper prototypes, sometimes video prototypes), parallel production of graphical components and behavior components, and final integration. The graphical components are produced with Inkscape or Adobe Illustrator and loaded from SVG files when the application is initialized, while the rest of the component hierarchy is created through the djnn APIs.

The most popular APIs are the Java API and a proprietary ObjectiveC API created by a user interface design company.

The main application of the XML formats so far has been to transform or verify programs that had been previously created by hand, not to execute models produced through controlled processes. This underlines the utility of performing property verification on executable programs without making assumptions on how these programs have been produced.

The verification of properties on djnn components is still experimental work and has not yet been integrated in the public releases. As explained previously, some properties are currently checked on the representation of the tree in memory when programs are launched and others on XML files using external tools. Each of these two approaches has proved useful. The external approach is useful for exploring properties and algorithms before considering an implementation in djnn. But it also helps to imagine solutions in which verifications are performed offline when modifications of programs are committed to version management systems or continuous integration systems. As for the internal approach, it also opens the door to verifications that would be performed at run time and not only when the program is initialized. For instance, verifications on the context such as checking what kind of display is available can be executed when the list of available displays changes, thus becoming part of the interactive program itself as proposed in [START_REF] Magnaudet | What should adaptivity mean to interactive software programmers?[END_REF].

In both cases, what the examples in this article illustrate is that interesting properties can be defined at the level of each component by programmers. There probably are general properties than must be checked for all programs, like what compilers propose for traditional programming languages. But, in the same vein as the verification of invariants in the programming-by-contract paradigm [START_REF] Meyer | Object-Oriented Software Construction[END_REF], there are many properties that are meaningful for a given component only, or for a given development team. This justifies supporting the management of such properties in languages and tools for interactive software. For instance, the XML format for djnn components can be enriched with new sections for each component, as in the example below:

<component name="graphics"> <xpath-required query="//sec" /> <circle name="bkg" cx="250" cy="250" r="100"/> <rotation name="r" cx="250" cy="250" a="0"/> <line name="sec" x1="250" y1="250" x2="250" y2="150"/> </component> These conditions, evaluated at verification time rather than run time, can be defined by designers or development teams before starting development, as a materialisation of a contract. Or they can be added by programmers during development, because they notice that they had to guarantee them even though they were not originally specified; doing so ensures non-regression for the future.

CONCLUSION

In this paper, we have developed an approach for the verification of interactive system properties based on static analysis and on the use of a language that describes interactive software as a hierarchy of interactive components. This approach transfers to interactive systems a method that is well known and used in other software domains. It gives the djnn framework the ability to support the formulation of component properties by members of development teams. Building abstract interpretations of djnn programs allows to check various properties automatically and directly on the code, whether they are related to design level or to system level. So far we have studied abstractions based on the component hierarchy, and more marginally on the control flow graph. Even if promising results have been obtained, a lot of further research is needed to explore the potential of this approach. Several research directions are currently under consideration. The range of properties expressible with XPaths must be explored as well as other methods for pattern matching in trees, including easier languages for expressing queries. It will also be useful to explore how well known graph properties and related algorithms can contribute to establishing useful properties, notably design structure matrix, graph traversal algorithms and graph covering problem. Another possible research area is how other abstractions built from the djnn model can be used for verification, for instance the data flow graph and the slicing approach.

Finally, we must explore what kind of design and development processes can be introduced for managing interactive software using these new possibilities. Contract-based development is an option, as well as incremental specification in parallel with prototype development. The extension of the proposed method to the verification of the compatibility of software with users' activities and tasks can also be explored.

As a final note, it should not be forgotten that it will be some time before the effective perception of an alarm can be proved, and not only its effective display. Empirical evaluation remains an important validation step for many systems.

Figure 1 .

 1 Figure 1. The order in the tree determines the graphical result

Figure 2 .

 2 Figure 2. How the djnn platform loads, executes and verifies the properties of components

Figure 3 .

 3 Figure 3. Two graphical designs for a clock verifying the same condition

Figure 4 .

 4 Figure 4. Checking the presence of an appropriate physical display

Figure 5 .

 5 Figure 5. Various representations of an animated program

Figure 6 .

 6 Figure 6. A primary flight display for aircraft cockpits

ACKNOWLEDGMENTS

This research was partly supported by the French DGAC through project FUMSECK and the EU ARTEMIS Joint Undertaking through project HoliDes (SP-8, GA No 332933). Any contents herein reflect only the authors' views. Neither DGAC not the ARTEMIS JU are liable for any use that may be made of the information contained herein.


Frédéric Didier
email: frederic.didier@inria.fr

Yann Laigle-Chapuy
email: laigle-chapuy@inria.fr

Finding low-weight polynomial multiples using discrete logarithm

Finding low-weight multiples of a binary polynomial is a difficult problem arising in the context of stream ciphers cryptanalysis. The best algorithms to solve this problem are based on a time memory tradeoff. Staying in this category, we will present a new approach using discrete logarithm rather than a direct representation of the involved polynomials. This provides an alternative to the previously known algorithms which improves in some case the computational complexity. 1

I. INTRODUCTION

Correlation and fast correlation attacks are probably the most important classes of attacks against stream ciphers based on linear feedback shift registers (LFSRs). They were originally proposed by Siegenthaler [START_REF] Siegenthaler | Cryptanalysts representation of nonlinearly filtered ml-sequences[END_REF] and improved by Meier and Staffelbach [START_REF] Meier | Fast correlation attacks on stream ciphers[END_REF]. Since then, many different versions have been proposed [START_REF] Canteaut | Improved fast correlation attacks using parity-check equations of weight 4 and 5[END_REF], [START_REF] Johansson | Improved fast correlation attack on stream ciphers via convolutional codes[END_REF], [START_REF] Johansson | Fast correlation attacks based on turbo code techniques[END_REF], [START_REF] Johansson | Fast correlation attacks through reconstruction of linear polynomials[END_REF], either very general or adapted to specific designs.

The basic idea is to consider that the output of the stream cipher is a noisy version of a sequence generated by an LFSR with the same initial state. The attack can be seen as an error-correction problem: recover the sequence, and therefore the initial state of the LFSR. To do this most of the attacks take advantage of parity check equations existing in the sequence we are trying to recover. Those parity check equations are in fact given by the multiples of the feedback polynomial, and to keep the bias as low as possible, low-weight multiples are necessary. As a precomputation step, we thus have to find those parity check equations before using them in the active part of the attack.

Depending on our objectives (finding one or many such multiples) and on the parameters (degree of the feedback polynomial and of the multiples, expected weight), there exists different algorithms to find lowweight multiples (see [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF], [START_REF] Finiasz | When stream cipher analysis meets public-key cryptography[END_REF]). We will complete them by another approach based on the use of discrete logarithm over finite fields. This will lead to a new algorithm for the computation of polynomials multiples that has better performance for some problems. Remark that the complexity of the best method is often still very high for parameters used in real cryptosystem. Notice also that in [START_REF] Penzhorn | Computation of low-weight parity checks for correlation attacks on stream ciphers[END_REF] discrete logarithms were already used to compute multiples of weight 3 and 4. We have generalized this idea and improved the complexity analysis.

The paper is organized as follows. Section II introduces some notations. The usual approach used to compute low-weight multiples is presented in Section III. In Section IV, we detail our main algorithm and compare its complexity with the algorithm of [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF]. Then, we will see in Section V how the complexity is modified when we only want to find a few multiples and not all. Finally, we will discuss in Section VI some important practical points and give some experimental results in Section VII.

II. PRELIMINARY

A. Notations

The problem we will be dealing with is the following.

Problem 1 (Low-weight polynomial multiple):

Input: A binary primitive polynomial P ∈ F 2 [X] of degree n, and two integers w and D.

Output: All the multiples of P of weight at most w and degree at most D.

The number of expected such multiples of P is heuristically approximated by D w-1 (w-1)!2 n , considering that for D large enough, the values of the polynomials of weight w and degree at most D are uniformly distributed.

Most of the time, the degree D and the weight are chosen high enough for many solutions to exist as we need many parity check equations to mount an attack.

It's also worth noticing that we almost never need all the multiples. In fact, to mount a successful attack, one only have to find a fixed number of parity check equations. It is thus sufficient to find many -but not all -multiples, which might be much easier, especially if the constraint on the degree and the weight are high enough. We therefore introduce a slightly different problem.

Problem 2: Input: A binary primitive polynomial P ∈ F 2 [X] of degree n, and three integers w, D and B.

Output: B multiples of P of weight at most w and degree at most D, or as much as possible if there are not B such multiples.

III. THE CLASSICAL APPROACH

A. The algorithm

The main idea is to use a time-memory trade-off (TMTO). Set w = q 1 + q 2 + 1 with q 1 ≤ q 2 . Algorithm 1 (TMTO):

• For all the q 1 -tuples Γ = (γ 1 , . . . , γ q1 ) with 0 < γ 1 < • • • < γ q1 ≤ D, compute and store the pairs

X γ1 + • • • + X γq 1 mod P ; Γ . • For all q 2 -tuples ∆ = (δ 1 , . . . , δ q2 ) with 0 < δ 1 < • • • < δ q2 ≤ D, compute X δ1 + • • • + X δq 2 mod P .
Look in the table for an element XORing to 1 (this can be efficiently done by using an hash table ).

If it exists, this gives

1 + γ∈Γ X γ + δ∈∆ X δ = 0 mod P.

B. Complexity

The usual time-memory trade-off is q 1 = w-1 2 and q 2 = w-1

2

, in order to balance the complexity of the two phases of the algorithm. The most time consuming part depends on the parity of w, as we do not have to compute anything to find the collisions if

q 1 = q 2 .
The memory complexity is then O (D q1 ) (for the first phase) while the time complexity is O (D q2 ). Remark that in [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF] the memory usage of the algorithm has been improved in order to use only O D ⌈ w-1 4 ⌉ bits.

IV. USING DISCRETE LOGARITHM

A. The algorithm

In this section, we will consider the field F 2 n defined as F 2 [x]/ P . The discrete logarithm (with base element x) in this field will be denoted by Log.

Set w = q 1 + q 2 + 2 with q 1 ≤ q 2 . Take two tuples

Γ = (γ 1 , . . . , γ q1 ) with 0 < γ 1 < • • • < γ q1 ≤ D and ∆ = (δ 1 , . . . , δ q2 ) with 0 < δ 1 < • • • < δ q2 ≤ D.
Denoting by L Γ and L ∆ the logarithms of 1 + γ∈Γ x γ and 1 + δ∈∆ x δ respectively, the following equalities hold in F 2 [x]/ P :

1 + γ∈Γ x γ = x LΓ-L∆ 1 + δ∈∆ x δ and x L∆-LΓ   1 + γ∈Γ x γ   = 1 + δ∈∆ x δ . Now let e ∈ ] -2 n-1 , 2 n-1 ] such that e is equal to L Γ -L ∆ modulo 2 n -1. If e > 0, then the polynomial   1 + γ∈Γ x γ   + x e 1 + δ∈∆ x δ (1)
is a multiple of P with degree max(γ q1 , δ q2 +e). If e < 0, then the polynomial

x -e   1 + γ∈Γ x γ   + 1 + δ∈∆ x δ (2)
is a multiple of P with degree max(γ q1 -e, δ q2 ). So, if one of the two following conditions is satisfied e > 0 and δ q2 + e ≤ D e < 0 and γ q1 -e ≤ D we get a multiple of P with degree at most D and weight at most w. We can rewrite both conditions in a single inequality

γ q1 -D ≤ e ≤ D -δ q2 . ( 3
)
The algorithm is then straightforward. Algorithm 2 (LogTMTO):

• For all the q 1 -tuples

Γ = (γ 1 , . . . , γ q1 ) with 0 < γ 1 < • • • < γ q1 ≤ D, compute L Γ = Log (1 + x γ1 + • • • + x γq 1 )
and store the pairs

L Γ ; Γ . • For all q 2 -tuples ∆ = (δ 1 , . . . , δ q2 ) with 0 < δ 1 < • • • < δ q2 ≤ D compute the logarithm L ∆ = Log 1 + x δ1 + • • • + x δq 2
and look in the table for all the elements with a logarithm L Γ satisfying (3). For each of them we obtain a multiple of P given by ( 1) or (2) depending on the sign of e. Of course, since we can decompose all polynomials of weight w in w-1 q1 way, we obtain each multiple many times.

B. Complexity

In order to perform the second phase, one could sort the table with increasing logarithms, but using an appropriate data structure like an hash table indexed by the most significants bits of the logarithm is a lot more efficient. As long as D < 2 n/2 , the search cost is O (1).

Once again, we choose the parameters of the timememory trade-off in order to balance the complexity of the two phases, taking q 1 = w-2 2 and q 2 = w-2

2

.

As for the classical algorithm, the most time consuming part depends on the parity of w as we do not have to compute any logarithm in the second phase if

q 1 = q 2 .
The memory usage is then O (D q1 ), while the time complexity is O (D q2 ) logarithm computations. We will see in Section VI-B that the logarithm can be computed quite efficiently. Actually for many practical values of n we can even compute it in O (1). Hence we neglect it in Table I.

TMTO D p D ⌈p/2⌉ D p D ⌈p/2⌉ LogTMTO D p-1 D p-1 D p D p-1
As we can see in Table I, if w is even we can improve the time complexity compared to the classical approach. Heuristically, the improvement by a factor D can be explained by the fact that we look for values in an interval of size roughly D instead of exact collisions.

Regarding the memory however, as explained in [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF] the computation behind the classical algorithm can be done using only O D ⌈p/2⌉ bits. So the discrete logarithms approach is always worse for odd w and will only be of practical interest when we are looking for all the multiples of weight 4 and maybe 6. After that, the memory usage just become too important.

However, we will see in the next section that when we are only looking for a small fraction of all the multiples of degree up to D, the discrete logarithms method can be quite efficient.

V. FIND MANY BUT NOT ALL

We deal in this section with the problem of finding a small proportion of all the multiples of weight w and degree at most D (Problem 2). If the number B of polynomials we want is small enough, depending on the parameters, we can do better than the previous algorithms.

A very basic approach is to try random polynomials of weight w until we actually find a multiple. In expectation we will then find a multiple every 2 n polynomials tried. We can also do the same using discrete logarithms. By computing logarithms for polynomials A of weight w-1 and degree less than D, we can obtain easily low-weight multiples of type A + x Log(A) if the logarithm is at most D. The expectation here is to find a multiple every 2 n /D iterations and we have won a factor D.

However, the best methods to solve this problem are once again TMTO. The algorithms are just simple variations of the previous ones when we put the elements in the hash table one by one and stop when we have found enough multiples.

the birthday paradox, we can thus find with the basic algorithm a multiple with a time and memory complexity of O √ 2 n in average. Using discrete logarithms, we will find a multiple as soon as two logarithms have a distance by approximately D. The complexity is then in O 2 n D both in time and memory. Remark that in this case one cannot use the improvement of [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF] to gain memory. There is also another approach based on Wagner's generalized birthday paradox (see [START_REF] Wagner | A generalized birthday problem[END_REF], [START_REF] Finiasz | When stream cipher analysis meets public-key cryptography[END_REF]) that can be usefull when w is large. Its complexity is in O 2 a 2 n/(a+1) for a a such that D (w-1)/2 a ≥ 2 n/(a+1) . As a conclusion to this section, when computing logarithms in F ⋆ 2 n is easy, we can gain a factor √ D in time and memory to find a multiple. Notice also that in practice when we need many multiples, we can design an algorithm between the one that compute all the multiples and the one presented here in order to get the best performance. We will see an illustration of this in Section VII.

VI. PRACTICAL CONSIDERATIONS

A. Bounds on the degree

First of all, it is worth noticing that it is not necessary to compute all the multiples up to the degree D to take all q 2 -tuples up to the degree D.

As a polynomial of weight w has many representations as a sum of a polynomial of weight q 1 + 1 and q 2 + 1 respectively, we can choose the one with the smallest q 2 -tuple.

Proposition 1: Let M = 1 + i∈I X i be a multiple of P of weight w = q 1 + q 2 + 2 and degree at most D.

Then there exists an integer 1 ≤ e ≤ D and two polynomials A and B of respective weight q 1 and q 2 and of degree respectively at most D and at most Dq2 w-1

such that M = (1 + A) + X e (1 + B) or X e (1 + A) + (1 + B) .
With the usual trade-off, we can restrict ourselves to the degree D/2, dividing the cost of the second phase approximately by a factor 2 w/2 .

B. How to compute logarithms

In practice, it is important to compute efficiently discrete logarithms in F ⋆ 2 n and hopefully there exists well studied algorithms to do that. It is important to take into account that we are going to compute many logarithms and not only one. All the efficient algorithms for computing logarithms (Baby-step Giant-step, Pohlig-Hellman algorithm [START_REF] Pohlig | An improved algorithm for computing logarithms over GF(p) and its cryptographic significance[END_REF] and Coppersmith algorithm [START_REF] Coppersmith | Evaluating logarithms in GF(2n)[END_REF], [START_REF] Coppersmith | Fast evaluation of logarithms in fields of characteristic two[END_REF]) can profit from a bigger precomputation step that can be done once and for all. For instance, if 2 n -1 is smooth enough, one can tabulate the logarithms in all the subgroups of F ⋆ 2 n to make the Pohlig-Hellman algorithm very efficient. In this case, a subsequent discrete logarithm computation can be done in O (1). This approach can be used for all the n up to 78 except {37, 41, 49, 59, 61, 62, 65, 67, 69, 71, 74, 77}. In addition we have listed in Table II some larger n for which it is applicable and the corresponding memory requirement. Notice that a full tabulation corresponds to a Giant-step of 1 and that by increasing a little this Giant-step, we can efficiently deal with more values of n . This leads to a very easy and efficient implementation as we will see in Section VII. Moreover, for the most useful cases (that is w ∈ {3, 4, 5}) we have to compute logarithms of the form Log 1 + x i . This logarithm is know as the Zech's logarithm of i, and we can exploit some properties of Zech's logarithm (see [START_REF] Huber | Some comments on zech's logarithms[END_REF]) to speed up the computation. Actually, by computing one Zech logarithm we get 6n other logarithms for free. Of course not all of them are useful for us, but the computation time can be divided by a factor of at least 2.

VII. EXPERIMENTAL RESULT

We have implemented our algorithm in C to test its efficiency. The computer used for our experiments is a 3.6GHz Pentium4 with 2MB of cache and 2GB of RAM.

A. Problem 1

We give in Table III As explained in the previous section, we used a fully tabulated Pohlig-Hellman. We can see that the algorithm is, as expected, very efficient for weight 4 as its complexity is linear in the degree D, both for time and memory (to be compared to a quadratic complexity for the classical approach).

We were also able to compute all the multiples of weight 5 and degree up to 2 16 of a polynomial of degree 53 within a few hours. But for the degree 5 the algorithm of [START_REF] Chose | Fast correlation attacks: an algorithmic point of view[END_REF] is more efficient.

B. Problem 2

With the same polynomial of degree n = 53, we also looked for multiples with an higher weight w = 7, and degree at most D = 2 15 . In order to do that, we precomputed all the trinomials (1 + x γ1 + x γ2 ) up to the degree K, which corresponds to q 1 = 2, instead of 3 for the optimal trade-off. We then computed many discrete logarithm of random polynomials (1+x δ1 +x δ2 + x δ3 + x δ4 ) in order to find multiples of weight 7. The results are given in Figure 1 where we see that a bigger precomputation can greatly improve the performance.

VIII. CONCLUSION

In this paper, we devised an algorithm to find lowweight multiples of a given binary polynomial that appears to be efficient for two cases that actually occur in practice.

The first case is when we are looking for all the multiples of weight 4 and degree at most D of a given polynomial of degree n. The complexity is then in O (D) discrete logarithms computation in F ⋆ 2 n where the other approach run in O D 2 . So the best algorithm will depends on the complexity of a discrete logarithm computation in F ⋆ 2 n which can be smaller than D in many practical situations. Notice that our algorithm may also give better performance for multiples of weight 6.

The other case where discrete logarithms can be useful is when we are only looking for a small fraction of all the possible multiples. The complexity to find one of them is then O 2 n D logarithm computations.

13 Fig. 1 .

 131 Fig.1. Evolution of the number of multiples of weight 7 and degree lower than 2 15 found with precomputed logarithms up to degree K

  the timings to find all the multiples of weight w up to degree D of the polynomial P = x 53 +x 47 +x 45 +x 44 +x 42 +x 40 +x 39 +x 38 +x 36 + x 33 +x 32 +x 31 +x 30 +x 28 +x 27 +x 26 +x 25 +x 21 +x 20 + x 17 +x 16 +x 15 +x 13 +x 11 +x 10 +x 7 +x 6 +x 3 +x 2 +x 1 +1.

TABLE III PROBLEM 1 :

 III1 FIND ALL THE MULTIPLES UP TO DEGREE D ′ 02 ′′ 1h52 ′ 4 ′ 11 ′′ 14 ′ 40 ′′ 3h33 ′

	n			53
	w		4			5
	log 2 (D)	20	22	28	13	14	16
	time	47 ′′ 2

This work is partially funded by CELAR/DGA.

ACKNOWLEDGMENT

The authors would like to thank Anne Canteaut and Jean-Pierre Tillich for their helpful insights on the subject.