Philippe Beaucamps
email: philippe.beaucamps@loria.fr

Isabelle Gnaedig
email: isabelle.gnaedig@loria.fr

Jean-Yves Marion
email: jean-yves.marion@loria.fr

Abstraction-based Malware Analysis Using Rewriting and Model Checking

Keywords: Malware, behavioral detection, behavior abstraction, trace, term rewriting, model checking, first order temporal logic, finite state automaton, formal language

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Behavior analysis was introduced by Cohen's seminal work [START_REF] Cohen | Computer viruses: Theory and experiments[END_REF] to detect malware and in particular unknown malware. In general, a behavior is described by a sequence of system calls and recognition uses the formalism of finite state automata [START_REF] Baudouin | Dynamic detection and classification of computer viruses using general behaviour patterns[END_REF][START_REF] Sekar | A fast automaton-based method for detecting anomalous program behaviors[END_REF][START_REF] Morales | Characterization of virus replication[END_REF][START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF]. New approaches have been proposed recently. In [START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Prabhat | Static verification of worm and virus behavior in binary executables using model checking[END_REF], malicious behaviors are specified by temporal logic formulas with parameters and detection is carried out by model-checking. However, these approaches are tightly dependent on the way malicious actions are realized: using any other system facility to realize an action allows a malware to go undetected. This has motivated yet another approach where a malicious behavior is specified as a combination of high-level actions, in order to be independent from the way these actions are realized and to only consider their effect on a system. In [START_REF] Martignoni | A layered architecture for detecting malicious behaviors[END_REF] and in [START_REF] Bayer | Scalable, Behavior-Based Malware Clustering[END_REF], a captured execution trace is transformed into a higher-level representation capturing its semantic meaning, i.e., the trace is first abstracted before being compared to a malicious behavior. In [START_REF] Jacob | Malware behavioral detection by attribute-automata using abstraction from platform and language[END_REF], the authors propose to use attribute automata, at the price of an exponential time complexity detection. These dynamic abstraction-based approaches, though they can detect unknown viruses whose execution traces exhibit known malicious behaviors, only deal with a single execution trace.

In this paper, we propose a formal approach for high-level behavior analysis, with the following features. Underpinned by language theory, term rewriting and first-order temporal logic, it allows us to determine whether a program exhibits a high-level behavior. Detection is achieved in two steps. First, traces of the program are abstracted in order to reveal the sequences of high-level functionalities they realize. Then, abstracted traces are compared with the behavior formula, using usual model-checking techniques. Functionalities have parameters representing the manipulated data, so our formalism is adapted to the protection against generic threats like the leak of sensitive information.

Our goal here is not to provide a ready-made software to detect behaviors, but to propose a formal framewok emphasizing fundamental detection mechanisms, which are independent of implementation-based solutions.

Our approach has two main characteristics. First, we work on an unbounded set of traces representing the behavior of a program, in order to consider a more complete representation of the program than with a single trace. To deal with the infinity of the set of traces, we restrict to regular sets and safely approximate the set of abstract traces, so that we detect in linear time whether a program exhibits a given behavior. Second, we work on abstract forms of traces, in order to only keep the essence of the functions performed by the program, to be independent of their possible implementations and to be generic with respect to behavior mutations. Behavior components are abstracted in program traces, by identifying known functionalities and marking them by inserting abstract functionality symbols.

By working on sets of traces, which may consist of a single trace as well as of an unbounded number of traces, our approach may be used not only for classical, dynamic behavior analysis, but also for static behavior analysis i.e., behavior analysis in a static analysis setting.

Static behavior analysis by abstraction is more challenging than its dynamic counterpart because, precisely, this approach needs to abstract a program behavior potentially representing an infinite set of execution traces. The construction of an exhaustive representation of a program behavior is an intractable problem in general: in particular, a program flow may not be easily followed due to indirect jumps, and a program may use complex code protection, for instance by dynamically modifying its code or by using obfuscation. Self modification is usually tackled by emulating the program long enough to deactivate most code protections. Indirect jumps and obfuscation are usually handled by abstract interpretation [START_REF] Dalla Preda | A semantics-based approach to malware detection[END_REF][START_REF] Kinder | An abstract interpretationbased framework for control flow reconstruction from binaries[END_REF] or symbolic execution [START_REF] Brumley | BitScope: Automatically dissecting malicious binaries[END_REF].

Static behavior analysis has many advantages and applications. First, it allows us to analyze the behavior of a program in a more exhaustive way, as it analyzes the unbounded set of the program execution traces, or an approximation of it. Second, static behavior analysis can complement classical, dynamic, behavior analysis with an analysis of the future behavior, to prevent damages when some critical point is reached in an execution.

An interesting application of static behavior analysis is the audit of programs in high-level technologies, like mobile applications, browser extensions, web page scripts, .NET or Java programs. Auditing these programs is complex and mostly manual, resulting in highly publicized infections [START_REF][END_REF][START_REF]Aftermath of the Droid Dream Android Market Malware Attack[END_REF]. In this context, static analysis can provide an appropriate help, because it is usually easier than for usual programs, especially when additionally enforcing a security policy (e.g. prohibiting self-modification [START_REF] Yee | Native client: A sandbox for portable, untrusted x86 native code[END_REF]) or when enforcing strict development guidelines (e.g. for iPhone applications).

To our knowledge, the use of behavior abstraction on top of static behavior analysis has not been investigated so far. As our detection mechanism relies on satisfaction of temporal logic formulas, it is akin to model checking [START_REF] Kröger | Temporal Logic and State Systems[END_REF], for which there already exist numerous frameworks and tools [START_REF] Holzmann | The SPIN Model Checker: Primer and Reference Manual[END_REF][START_REF] Garavel | Cadp 2010: A toolbox for the construction and analysis of distributed processes[END_REF][START_REF] Chen | MOP: An Efficient and Generic Runtime Verification Framework[END_REF]. The specificity of our approach, however, is that, rather than being applied on the set of program traces, verification is applied on the set of abstract forms of these traces, which is not computable in general. Accordingly, we identify a property of practical highlevel behaviors allowing us to approximate this set, in a sound and complete way with respect to detection, and then to apply classical verification techniques.

Our abstraction framework can be used in two scenarios:

-Detection of given behaviors: signatures of given high-level behaviors are expressed in terms of abstract functionalities. Given some program, we then assess whether one of its execution traces exhibits a sequence of known functionalities, in a way specific to one of the given behaviors. This can be applied to detection of suspicious behaviors. Although detection of such suspicious behaviors may not suffice to label a program as malicious, it can be used to supplement existing detection techniques with additional decision criteria. -Analysis of programs: abstraction provides a simple and high-level representation of a program behavior, which is more suitable than the original traces for manual analysis, or for analysis of behavior similarity with known behaviors, etc. For instance, it could be used to detect not necessarily harmful behaviors, in order to get a basic understanding of the program and to further investigate if deemed necessary. It could also be used to automatically discover sequences of high-level functionalities and their dataflow dependencies, exhibited by a program.

Previous work.

In [START_REF] Beaucamps | Behavior Abstraction in Malware Analysis[END_REF], we already proposed to abstract program sets of traces with respect to behavior patterns, for detection and analysis. We tested our approach on samples of malicious programs collected using a honeypot3 and identified using Kaspersky Antivirus. These samples belonged to known malware families, like Allaple, Virut, Agent, Rbot, Afcore and Mimail. Most of them were successfully matched to our malware database.

But patterns were defined by string rewriting systems, which did not allow the actions composing a trace to have parameters, precluding dataflow analysis. Moreover, abstraction rules replaced identified patterns by abstraction symbols in the original trace, precluding a further detection of patterns interleaved with the rewritten ones.

The formalism proposed in this paper addresses both issues: first, we handle interleaved patterns by keeping the identified patterns when abstracting them. Second, we extend the rewriting framework to express data constraints on action parameters by using term rewriting systems. An important consequence is that, unlike in [START_REF] Beaucamps | Behavior Abstraction in Malware Analysis[END_REF], using the dataflow, we can detect information leaks in order to prevent unauthorized disclosure or modifications of information.

Background

Term Algebras. Let S = {T race, Action, Data} be a set of sorts, F = F t ∪ F a ∪F d be a finite S-sorted signature, where F t , F a , F d are mutually distinct and:

-F t = {ǫ, •} is the set of the trace constructors, where ǫ :→ T race denotes the empty trace, . has profile Data T race → T race; -F a is a set of function symbols or constants, with profile Data n → Action, n ∈ N, describing actions; -F d is a set of data constructors, with profile → Data or Data n → Data, n ∈ N.

Let N * + be the set of finite strings of positive natural numbers, called positions. The empty string is denoted by λ, and u ≤ v means that u is prefix of v. Let X be a set of S-sorted variables. A S-sorted term over (F, X) is a partial function t : N * + → F ∪ X, such that the domain of definition of t, denoted by Pos(t), is finite and satisfies, for w ∈ N * + and i ∈ N: (1) wi ∈ Pos(t) ⇒ w ∈ Pos(t), (2) w ∈ Pos(t) ⇒ t(w) ∈ F ∪ X. Pos(t) is called the set of positions of t. We denote by T (F, X) (resp. T (F)) the set of S-sorted terms over (F, X) (resp. the set of finite ground terms over F). For any sort s ∈ S, and any of the above sets of terms T we denote by T s the restriction of T to terms of sort s and by X s the subset of variables of X of sort s. For a term t with p ∈ Pos(t), we denote by t| p the subterm of t at position p. We denote by t[t ′ ] p the term obtained by replacing by t ′ the subterm at position p in t. We use the abbreviated notation x for variables x 1 , . . . , x n . So x ∈ X stands for x 1 , . . . , x n ∈ X, and if f ∈ F is a symbol of arity n ∈ N, we denote by f (x) the term f (x 1 , . . . , x n ).

The elements of T Trace (F) are called traces, the elements of T Action (F) are called actions. We distinguish the sort Action from the sort Trace but, for a sake of readability, we may denote by a the trace • (a, ǫ), for some action a. Similarly, we use the • symbol with infix notation and right associativity, and ǫ is understood when the context is unambiguous. For instance, if a, b, c are actions, a

• b • c denotes the trace • (a, • (b, • (c, ǫ))).
We partition F a in a set Σ of symbols, denoting concrete program-level actions, and a set Γ , denoting abstract actions identifying abstracted functionalities. To construct purely concrete (resp. abstract) terms, we use F Σ = F \ Γ (resp. F Γ = F \ Σ). The projection t| Σ ′ , also denoted π Σ ′ (t), of a trace t on an alphabet Σ ′ ⊆ F a corresponds to keeping in a trace only actions from Σ ′ . If X is a set of variables of sort Data, we define the projection on an alphabet Σ ′ ⊆ F a of a term t ∈ T Trace (F, X), denoted by π Σ ′ (t) or, equivalently, by t| Σ ′ , in the following way:

π Σ ′ (ǫ) = ǫ π Σ ′ (b • u) = b • π Σ ′ (u) if b ∈ T Action (F Σ ′ , X) π Σ ′ (u) otherwise with b ∈ T Action (F, X) and u ∈ T Trace (F, X).
The projection is naturally extended to sets of traces.

We define in a natural way the concatenation t • t ′ of two traces t and t ′ . The concatenation of two terms t and t ′ of T Trace (F, X), where X is a set of S-sorted variables and t ∈ X, is denoted by t•t ′ ∈ T Trace (F, X) and defined by t•t ′ = t [t ′ ] p , where p is the position of ǫ in t, i.e., t| p = ǫ. Projection and concatenation are naturally extended to sets of terms of sort Trace. We also extend concatenation to 2 TTrace(F,X) ×2 TTrace(F,X) with L

•L ′ = {t • t ′ | t ∈ L, t ′ ∈ L ′ } and to 2 TTrace(F,X) × T Action (F, X) with L • a = L • {a • ǫ}.
Substitutions are defined as usual. A ground substitution on a finite set X of S-sorted variables is a mapping σ : X → T (F) such that: ∀s ∈ S, ∀x ∈ X s , σ (x) ∈ T s (F). σ can be naturally extended to a mapping T (F, X) → T (F) in such a way that:

∀f (t 1 , . . . , t n ) ∈ T (F, X) , σ (f (t 1 , . . . , t n )) = f (σ (t 1 ) , . . . , σ (t n )) .
By convention, we denote by tσ or by σ (t) the application of a substitution σ to a term t ∈ T (F, X) and by Lσ the application of σ to a set of terms L ⊆ T (F, X). The set of ground substitutions over X is denoted by Subst X .

Program Behavior. The representation of a program is chosen to be its set of traces. When executing a program, the captured data is represented on the alphabets Σ, denoting the concrete actions, and F d , describing the data. In this paper, we consider that the captured data is the library calls along with their arguments. Σ therefore represents the finite set of library calls, while terms built on F d identify the arguments and the return values of these calls. A program execution trace then consists of a sequence of library calls and is defined by a term of T Trace (F Σ ). A program behavior is defined by the set of its execution traces, that is a possibly infinite subset of T Trace (F Σ ). First-Order Linear Temporal Logic (FOLTL). We consider the First-Order Logic (FOLTL) defined in [START_REF] Kröger | Temporal Logic and State Systems[END_REF], without the equality predicate, where the set of atomic predicates AP is a set of terms with variables in a set X. FOLTL is an extension of the LTL Logic (see also [START_REF] Kröger | Temporal Logic and State Systems[END_REF]) such that:

-If ϕ is an LTL formula, then ϕ is an FOLTL formula; -If ϕ is an FOLTL formula and Y ⊆ X is a set of variables, then: ∃Y.ϕ and ∀Y.ϕ are FOLTL formulas, where as usual: ∀Y.ϕ ≡ ¬∃Y.¬ϕ.

Notation ϕ 1 ⊙ ϕ 2 stands for ϕ 1 ∧ X (⊤ U ϕ 2 ).
We say that a FOLTL formula is closed when it has no free variable, i.e., every variable is bound by a quantifier.

Let Y ⊆ X be a set of variables of sort Data and σ ∈ Subst Y be a ground substitution over Y . The application of σ to an FOLTL formula ϕ is naturally defined by the formula ϕσ where any free variable x in ϕ which is in Y has been replaced by its value σ (x).

A formula ϕ is satisfied on infinite sequences of sets of ground instances of atomic predicates, denoted by ξ = (ξ 0 , ξ 1 , . . .). ξ |= ϕ (ξ satisfies ϕ) is defined in the same way as for the LTL logic, with the additional rule: ξ |= ∃Y.ϕ iff there exists σ ∈ Subst Y such that ξ |= ϕσ.

In our context, a formula is satisfied over traces of T Trace (F) identified with sequences of singleton sets of atomic predicates. A finite trace t = a 0 • • • a n is identified with the infinite sequence of sets of atomic predicates ξ t = ({a 0 } , . . . , {a n } , {} , {} , . . .), and t satisfies ϕ, denoted by t |= ϕ, iff ξ t |= ϕ.

We consider two distinct instances of this logic, depending on the fact that we consider concrete traces or abstract traces. We denote by FOLTL Σ the FOLTL logic, where the set of atomic predicates is AP Σ = T Action (F Σ , X) and ξ is in 2 TAction(FΣ) ω . We denote by FOLTL Γ the FOLTL logic, where the set of atomic predicates is AP Γ = T Action (F Γ , X) and ξ is in 2 TAction(FΓ) ω .

Note that in practice, to express behaviors, we only use FOLTL formulas that are negations of safety properties. We do not use properties with liveness aspects, which would note make sense on finite traces. Using FOLTL on finite traces allows us a correct balance between behavior expresivity and decidability.

Tree automata and tree transducers are defined as usual [START_REF] Comon | Tree automata techniques and applications[END_REF].

Behavior Patterns

The problem under study can be formalized in the following way. First, using FOLTL formulas, we define a set of behavior patterns, where each pattern represents a (possibly infinite) set of terms from T Trace (F Σ ). Second, we need to define a terminating abstraction relation R allowing to schematize a trace by abstracting occurrences of the behavior patterns in that trace. Finally, given some program p coming with an infinite set of traces L (static analysis scenario, for instance by using the control flow graph, see our previous work [START_REF] Beaucamps | Behavior Abstraction in Malware Analysis[END_REF] and [START_REF] Christodorescu | Semantics-aware malware detection[END_REF][START_REF] Kirda | Behavior-based Spyware Detection[END_REF]), we formulate the detection problem in the following way. Let L↓ R be the set of normal forms of traces of L for R i.e., the set of abstracted traces of L, using R. Given an abstract behavior M defined by an FOLTL formula ϕ, does there exist a trace t in L↓ R such that t |= ϕ? Our goal is then to find an effective and efficient method solving this problem.

A behavior pattern describes a functionality we want to recognize in a program trace, like writing to system files, sending a mail or pinging a remote host. Such a functionality can be realized in different ways, depending on which system calls, library calls or programming languages it uses.

We describe a functionality by an FOLTL formula, such that traces satisfying this formula are traces carrying out the functionality.

Example 1. Let us consider the functionality of sending a ping. One way of realizing it consists in calling the socket function with the parameter IPPROTO ICMP describing the network protocol and, then, calling the sendto function with the parameter ICMP ECHOREQ describing the data to be sent. Between these two calls, the socket should not be freed. This is described by the FOLTL formula:

ϕ 1 = ∃x, y. socket (x, α) ∧ (¬closesocket (x) U sendto (x, β, y))
, where the first parameter of socket is the created socket and the second parameter is the network protocol, the first parameter of sendto is the used socket, the second parameter is the sent data and the third one is the target, the unique parameter of closesocket is the freed socket and constants α and β in F d identify the above parameters IPPROTO ICMP and ICMP ECHOREQ.

A ping may also be realized using the function IcmpSendEcho, whose parameter represents the ping target. This corresponds to the FOLTL formula:

ϕ 2 = ∃x. IcmpSendEcho (x).
Hence, the ping functionality may be described by the FOLTL formula:

ϕ ping = ϕ 1 ∨ ϕ 2 .
We then define a behavior pattern as the set of traces carrying out its functionality i.e., satisfying the formula describing the functionality.

Definition 1. A behavior pattern is a set of traces B ⊆ T Trace (F Σ ) satisfying a closed FOLTL Σ formula ϕ: B = {t ∈ T Trace (F Σ ) | t |= ϕ} .

Trace Abstraction

As said before, our goal is to be able to detect, in a given set of traces, some predefined behavior composed of combinations of high-level functionalities. For this, we associate to each behavior pattern an abstract symbol λ taken in the alphabet Γ , called abstraction symbol. An abstract behavior is then defined by combinations of abstraction symbols associated to behavior patterns, using an FOLTL formula ϕ on

AP Γ = T Action (F Γ , X) instead of AP Σ = T Action (F Σ , X). Definition 2. An abstract behavior is a set of traces M ⊆ T Trace (F Γ ) satisfying a closed FOLTL Γ formula ϕ M : M = {t ∈ T Trace (F Γ ) | t |= ϕ M } . When M is defined by a formula ϕ M , we write: M := ϕ M .
Example 2. The abstract behavior of sending a ping to a remote host can then be trivially defined by the formula: ϕ M = ∃x. F λ ping (x) .

In the following, for the sake of simplicity, the initial F operator is implicit in definitions of abstract behaviors. Now, let L be the set of program traces we want to analyze. To compare these traces to the given abstract behavior, we have to consider the behavior pattern occurrences they may contain, at the abstract level. For this, we define an abstraction relation R, which marks such occurrences in traces by inserting an abstraction symbol λ B when an occurrence of the behavior pattern B is identified.

From now on, if a behavior pattern is defined using an FOLTL formula ϕ and associated to an abstraction symbol λ, we may denote it λ := ϕ.

The abstraction symbol can have parameters corresponding to those used by the behavior pattern. This allows us to express dataflow constraints in a signature. For instance, the abstraction symbol for the ping behavior pattern can take a parameter denoting the ping target. A signature for a denial of service could then be defined, for example, as a sequence of 100 pings with the same target.

Example 3. The ping behavior pattern in Example 1 is abstracted in traces by inserting the λ ping symbol after the send action or after the IcmpSendEcho action. Then, the trace socket(1, α)

• gethostbyname(2) • sendto(1, β, 3) • closesocket(1) can be abstracted into the trace socket(1, α) • gethostbyname(2) • sendto(1, β, 3) • λ ping (3) • closesocket(1).
Thus, abstraction of a trace reveals abstract behavior pattern combinations, which may constitute the abstract behavior to be observed. We now formally define the abstraction relation.

As said above, abstracting a trace with respect to some behavior pattern amounts to transforming it when it contains an occurrence of the behavior pattern, by inserting a symbol of Γ in the trace. This symbol is inserted at the position after which the behavior pattern functionality has been performed. This position is the most logical one to stick to the trace semantics. Furthermore, when behavior patterns appear interleaved, this position allows us to define the order in which their functionalities are realized (see the full version of the paper for an example [START_REF] Beaucamps | Behavior Analysis of Malware by Rewriting-based Abstraction -Extended Version[END_REF]).

As said in the introduction, rather than replace behavior pattern occurrences with abstraction symbols, we preserve them in order to properly handle interleaved behavior patterns occurrences. Now, let us consider the following example.

Example 4. Abstraction of the ping in Example 3 is realized by rewriting using the rule

A 1 (x, y) • B 1 (x, y) → A 1 (x, y) • λ(y) • B 1 (x, y), where A 1 (x, y) = socket(x, α) • (T Trace (F Σ ) \ (T Trace (F Σ ) • closesocket(x) • T Trace (F Σ ))) • sendto(x, β, y) and B 1 (x, y) = {ǫ}, and the rule A 2 (x) • B 2 (x) → A 2 (x) • λ(x) • B 2 (x), where A 2 (x) = {IcmpSendEcho(x)} and B 2 (x) = {ǫ}.
As a behavior pattern is a set of possible traces realizing a given functionality, we define the abstraction relation by decomposing the behavior pattern into a finite union of concatenations of sets A i (X) and B i (X) such that traces in A i (X) end with the action effectively performing the behavior pattern functionality. These sets A i (X) and B i (X) are composed of concrete traces only, since abstract actions that may appear in a partially rewritten trace should not impact the abstraction of an occurrence of the behavior pattern. Definition 3. Let λ ∈ Γ be an abstraction symbol, X be a set of variables of sort Data, x be a sequence of variables in X. An abstraction system on T Trace (F, X) is a finite set of rewrite rules of the form:

A i (X)•B i (X) → A i (X)•λ (x)•B i (X)
where the sets A i (X) and B i (X) are sets of concrete traces of T Trace (F Σ , X).

Dealing with sets as left(right)-hand sides of rules may seem to be heavy. In fact, this allows us to recognize not only finitely enumerated patterns, but patterns from languages i.e., patterns among possibly infinite sets of behaviors.

The system of rewrite rules we use generates a reduction relation on T Trace (F) such that filtering works on traces projected on Σ. Definition 4. The reduction relation on T Trace (F) generated by a system of n rewrite rules

A i (X) • B i (X) → A i (X) • λ (x) • B i (X) is the rewriting relation → R such that, for all t, t ′ ∈ T Trace (F) , t → R t ′ iff: ∃σ ∈ Subst X , ∃p ∈ Pos(t), ∃i ∈ [1..n] , ∃a ∈ T Trace (F) • T Action (F Σ ) , ∃b, u ∈ T Trace (F), a| Σ ∈ A i (X) σ, b| Σ ∈ B i (X) σ, t| p = a • b • u and t ′ = t [a • λ (x) σ • b • u] p .
An abstraction relation with respect to a given behavior pattern is thus the reduction relation of an abstraction system, where left members of the rules cover the set of the traces realizing the behavior pattern functionality. Definition 5. Let B be a behavior pattern associated with an abstraction symbol λ ∈ Γ . Let X be a set of variables of sort Data. An abstraction relation w.r.t. this behavior pattern is the reduction relation on T Trace (F Σ ) generated by an abstraction system composed of n rules A i (X)

• B i (X) → A i (X) • λ (x) • B i (X) verifying: B = i∈[1..n] σ∈SubstX (A i (X) • B i (X)) σ .
Finally, we generalize the definition of abstraction to a set of behavior patterns. As we will see later, for R to be realizable by a tree transducer, the abstraction relation R has to be terminating. However, even with a finite set of traces, abstraction does not terminate in general, since the same occurrence of a pattern can be abstracted an unbounded number of times. So we require that the same abstract action is not inserted twice after the same concrete action. In other words, if t = t 1 •t 2 is abstracted into t ′ = t 1 •α•t 2 , where α is the inserted abstract action, then if t 2 starts with a sequence of abstract actions, α does not appear in this sequence. Formally, we require that:

∀t 1 , t 2 ∈ T Trace (F) , ∀α ∈ T Action (F Γ ), if t 1 • t 2 → R t 1 • α • t 2 , then ∃u ∈ T Trace (F Γ ) , ∃u ′ ∈ T Trace (F) , t 2 = u • α • u ′ .
Using the above condition, supposed to be verified from now on, a behavior pattern occurrence can only be abstracted once. Furthermore, abstraction does not create new abstraction opportunities so the relation R is clearly terminating. Remark 1. A terminating abstraction relation with respect to a set of behavior patterns is not confluent in general. We could adapt the definition of the abstraction relation to make it confluent, for instance by defining an order on the set T Action (F Γ ). However, as already mentioned, detection works on normal forms. So having several normal forms for a trace does not compromise its mechanism.

In practice, a behavior pattern is regular, along with the set of instances of right-hand sides of its abstraction rules. We show that this is sufficient, with termination of the set of rules, to ensure that the abstraction relation is realizable by a tree transducer, in other words that it is a rational tree transduction. The tree transducer formalism is chosen for its interesting formal (closure by union, composition, preservation of regularity) and computational properties. When T Action (F) is finite, we can state the following result.

Theorem 1. Let B be a behavior pattern and R be a terminating abstraction relation w.r.t. B defined by an abstraction system whose set of instances of righthand sides of rules is recognized by a tree automaton A R . Then R and R -1 are rational and, for any tree automaton A recognizing a trace language L, R(L) is recognized by a tree automaton of size O (|A| • |A R |).

Detection Problem

Then the detection problem can be formalizeded as follows. Definition 7. A set of traces L ⊆ T Trace (F Σ ) exhibits an abstract behavior M defined by a formula ϕ M , denoted by

L ⋓ M , iff: ∃t ∈ L↓ R | Γ , t |= ϕ M .
When L is restricted to a single trace, or to a finite set of traces, like in dynamic analysis, the set L↓ R of normal forms of traces i.e., the set of traces that cannot be rewritten anymore with R, is computable since the rewrite system R is terminating. Moreover, as FOLTL quantification is performed over variables in the domain T Data (F), FOLTL verification is decidable when T Data (F) is finite. So in this case, it can be decided whether L exhibits M .

For an infinite set of finite traces L however, the computation of L↓ R often relies on the computation of the set of descendants R * (L) of L i.e., the set of all terms that can be rewritten from terms of L. But R * (L) is computable only for some classes of rewrite systems [START_REF] Gilleron | Regular Tree Languages and Rewrite Systems[END_REF] and when L is regular. Unfortunately, the rewrite systems which implement the abstraction relations and which are described in Sect. 4 do not belong to any of these classes. Hence, we cannot rely on the construction of L↓ R to decide whether L exhibits M .

Nevertheless, we will see that, for behaviors considered in practice, a partial abstraction of the set of traces is sufficient i.e., computing the set of normal forms is unnecessary. We therefore propose a detection algorithm relying on a safe approximation of the set of abstract traces. This approximation must be chosen carefully. For instance, it cannot consist in computing, for some n, the set R ≤n (L) of descendants of L until order n, as shown by the following example.

Example 5. Let λ 1 := a, λ 2 := b, λ 3 := c be three behavior patterns associated to abstraction relations inserting the abstraction symbol after a, b and c respectively. Let M := λ 1 ∧ (¬λ 2 U λ 3 ) be an abstract behavior. Assume there exists a bound n such that L↓ R may be approximated by

R ≤n (L) in Definition 7. The trace t = a n-1 • b • c • d does not exhibit the behavior M . Yet the trace t ′ = (a • λ 1 ) n-1 • b • c • λ 3 • d is in R ≤n ({t})
and its projection on Γ is in M , so we would wrongly infer that t exhibits M .

The problem comes from the fact that R ≤n (L) contains contradictory traces compromising detection i.e., traces seemingly exhibiting an abstract behavior though a few additional abstraction steps would make them leave the signature.

Consequently, we want to exclude traces unreliably realizing the abstract behavior in R ≤n (L), while not having to reach normal forms. In fact, we identify a fundamental property we call (m, n)-completeness, verified by abstract behaviors in practice in the field of malware detection. This property states that, for a program to exhibit an abstract behavior, a necessary and sufficient condition is the following: there exists a partially abstracted trace, abstracted in at most m abstraction steps, realizing the behavior and whose descendants until the order n still realize it. Definition 8. Let M be an abstract behavior defined by a formula ϕ M and m and n be positive numbers. M has the property of (m, n)-completeness iff for any set of traces L ⊆ T Trace (F Σ ):

L ⋓ M ⇔ ∃t ′ ∈ R ≤m (L), ∀t ′′ ∈ R ≤n (t ′ ) Γ , t ′′ |= ϕ M .
We then show in the next section that, when L is regular, there exists a sound and complete detection procedure for every abstract behavior enjoying this property. Moreover, the time and space complexity of this detection procedure is linear in the size of the representation of L.

The following propositions show that the (m, n)-completeness property is realistic for abstract behaviors considered in practice.

We first prove, for particular abstract behaviors describing sequences of abstract actions with no constraints other than dataflow constraints, that we have the property of (m, n)-completeness.

Proposition 1. Let Y be a set of variables of sort Data. Let α 1 , . . . , α m ∈ T Action (F Γ , Y ). Then the abstract behavior M := ∃Y. α 1 ⊙α 2 ⊙ . . . ⊙ α m has the property of (m, 0)-completeness.

Proofs of propositions and theorems can be found in [START_REF] Beaucamps | Behavior Analysis of Malware by Rewriting-based Abstraction -Extended Version[END_REF]. We now show that more complex abstract behaviors, forbidding specific abstract actions, have this property.

For a behavior pattern λ, let R λ denote the restriction of the abstraction relation R to abstraction with respect to λ. We say that two behavior patterns λ and λ ′ are independent iff:

R λ • R λ ′ = R λ ′ • R λ .
Then we get the following result.

Proposition 2. Let M := ∃Y. λ 1 (x 1 ) ∧ ¬(∃Z. λ 2 (x 2 )) U λ 3 (x 3 ) be an abstract behavior where Y and Z are two disjoint sets of variables of sort Data, x 1 , x 3 ∈ Y , x 2 ∈ Z, and where λ 2 = λ 1 , λ 2 = λ 3 and λ 2 is independent from λ 3 . Then M has the property of (2, 1)-completeness.

In practice, as illustrated in Sect. 7, most signatures are disjunctions of formulas of the form: ∃Y. α 1 ⊙ α 2 ⊙ . . . ⊙ α m , from Proposition 1, or of the form:

∃Y.λ 1 (x 1 ) ∧ ¬ (∃Z 1 . λ (z 1 )) U λ 2 (x 2 ) ∧ ¬ (∃Z 2 . λ (z 2 )) U . . . λ k (x k )
where λ is independent from λ 2 , . . . , λ k . From the proof of Proposition 2, we conjecture that the last formula has the property of (k, 1)-completeness.

The independence condition is not necessary in general, in order to guarantee that such abstract behaviors have a property of (m, n)-completeness for some m and n, but absence of this condition results in significantly higher values of m and n.

Fundamentally, by Definition 7, detection of an abstract behavior is decomposed into two independent steps: an abstraction step followed by a verification step. The first step computes the abstract forms of the program traces while the second step applies usual verification techniques in order to decide whether one of the computed traces verifies the FOLTL formula defining the abstract behavior. However, when using the (m, n)-completeness property to bypass the general intractability of the abstraction step, this relies on computing a set t ∈ T Trace (F) , R ≤n (t) |= ϕ M and then intersecting it with R ≤m (L). So we lose the previous decomposition, thereby preventing us from leveraging powerful techniques from the model checking theory. We therefore show that, in the previous proposition, (m, n)-completeness allows us to nonetheless preserve that decomposition, so that the abstraction step now becomes decidable.

Theorem 2. Let M be an abstract behavior defined by a formula ϕ M = ∃Y. λ 1 (x 1 ) ∧ ¬(∃Z. λ 2 (x 2 )) U λ 3 (x 3 ) where Y and Z are disjoint sets of variables of sort Data, x 1 , x 3 ∈ Y , x 2 ∈ Z, and where λ 2 = λ 1 , λ 2 = λ 3 and λ 2 is independent from λ 3 . Then, for any set of traces L ⊆ T Trace (F Σ ), L exhibits M iff:

∃t ∈ R λ2  (R ≤2 (L)) Γ , t |= ϕ M .
When both the abstraction relation R and the relation R λ2  are rational, the set R λ2  (R ≤2 (L)) is computable and regular, and detection then boils down to a classical model checking problem. In the general case, R λ2  is not rational, but in our experimentations, the behavior pattern λ 2 is defined by sets A i and B i where A i contains traces made of a single action and B i = {ǫ}. Thus constructing a transducer realizing the relation R λ2  is straightforward.

Remark 2. An equivalent definition of infection could consist in compiling the abstract behavior, that is computing the set π -1 Γ (M )  R -1 of concrete traces exhibiting M . Then a set of traces L would exhibit M iff one of its traces is in this set. This definition seems more intuitive: rather than abstracting a trace and comparing it to an abstract behavior, we check whether this trace is an implementation of the behavior. However, this approach would require to first compute the compiled form of the abstract behavior, π -1 Γ (M )  R -1 , which is not generally computable and whose representation can quickly have a prohibitive complexity stemming from the interleaving of behavior patterns occurrences (especially when traces realizing the behavior patterns are complex) and from the variable instantiations.

Detection Complexity

The detection problem, like the more general problem of program analysis, requires computing a partial abstraction of the set of analyzed traces. In practice, in order to manipulate this set, we consider a regular approximation of it i.e., a tree automaton. Moreover, in practice, as seen in Sect. 4, the abstraction relation is rational, which entails the decidability of detection.

Theorem 3. Let R be an abstraction relation, such that R and R -1 are rational. There exists a detection procedure deciding whether L exhibits M , for any regular set of traces L ⊆ T Trace (F Σ ) and for any regular abstract behavior M having the property of (m, n)-completeness for some positive integers m and n. Definition 9. Let M be an abstract behavior having the property of (m, n)completeness. The set of traces n-reliably realizing M w.r.t an abstraction relation R is the set {t

∈ T Trace (F) | ∀t ′ ∈ R ≤n (t) Γ , t ′ |= ϕ M }.
Using the set of traces n-reliably realizing M , when T Action (F) is finite, we get the following detection complexity, which is linear in the size of the automaton recognizing the program set of traces, a major improvement on the exponential complexity bound of [START_REF] Jacob | Malware behavioral detection by attribute-automata using abstraction from platform and language[END_REF].

Information Leak Behaviors

Abstraction can be applied to detection of generic threats, and in particular to detection of sensitive information leak. Such a leak can be decomposed into two steps: capturing sensitive information and sending this information to an exogenous location. The captured data can be keystrokes, passwords or data read from a sensitive network location, while the exogenous location can be the network, a removable device, etc. Thus, we define a behavior pattern λ steal (x), representing the capture of some sensitive data x, and a behavior pattern λ leak (x), representing the transmission of x to an exogenous location. Moreover, since the captured data must not be invalidated before being leaked, we define a behavior pattern λ inval (x), which represents such an invalidation. Finally, the captured data is usually not leaked in its raw form, so we take into account transformations of this data via the behavior pattern λ depends (x, y) which denotes a dependency of x on y. For instance, x may be a string representation of y, or x may be an encryption or an encoding of y.

Then, in order to account for one such transformation of the stolen data, we define the information leak abstract behavior: M := ∃x, y. λ steal (x) ∧ ¬λ inval (x) U λ depends (y, x) ∧ U λ leak (y) .

We consider the following definitions of the four behavior patterns involved, after looking at several malware samples, like keyloggers, sms message leaking applications or personal information stealing mobile applications:

keystroke capture functionality:

Experiments

Our goal is to detect the information leak behavior M defined in the previous section. In order to perform behavior pattern abstraction and behavior detection in the presence of data, we use the CADP toolbox [START_REF] Garavel | Cadp 2010: A toolbox for the construction and analysis of distributed processes[END_REF], which allows us to manipulate and model-check communicating processes written in the LO-TOS language. CADP features a verification tool, which allows on-the-fly model checking of formulas expressed in the MCL language, a fragment of the modal mu-calculus extended with data variables, whose FOLTL logic used in this paper is a subset.

We first represent the program set of traces as a CADP process, using a program control flow graph obtained by static analysis (see [START_REF] Beaucamps | Behavior Abstraction in Malware Analysis[END_REF] and [START_REF] Christodorescu | Semantics-aware malware detection[END_REF][START_REF] Kirda | Behavior-based Spyware Detection[END_REF]). Regularity of the set of traces is enforced by limiting recursion and inlining function calls, an approximation that can be deemed safe with respect to the abstract behaviors to detect. Note that there are two shortcomings to regular approximation. First, approximation of conditional branches by nondeterministic branches may result in false positives, especially when the program code is obfuscated. And second, failure to identify data correlations during dataflow analysis can result in false negatives. However, this does not significantly impact our detection results. Now, as expressed in Theorem 2, detection of the information leak abstract behavior M can be broken down into two steps: abstracting the set of traces L by computing R λ inval  R ≤2 (L) and then verifying whether an abstracted trace matches the abstract behavior formula.

So, we can simulate the abstraction step in CADP and delegate the verification step to the evaluator4 module. For this, we represent the set of traces L of a given program by a system of communicating processes expressed in LO-TOS, with a particular gate on which communications correspond to library calls. Then, computation of R ≤2 (L) is performed by synchronization with another LOTOS process which simulates the transducer realizing the abstraction. Moreover, the relation R λ inval  is rational and can also be simulated by process synchronization in CADP.

For each malware sample we tested, we successfully ran evaluator4 on the resulting process representing R λ inval  (R ≤2 (L)), in order to detect the information leak abstract behavior defined in the previous section.

We essentially applied our approach to two case studies. The first one comes from a study on the detection rate of keylogger programs by existing antivirus [START_REF] Devine | A study of anti-virus' response to unknown threats[END_REF], which shows a high failure rate. For an example of a typical keylogger for test, see [START_REF] Beaucamps | Behavior Analysis of Malware by Rewriting-based Abstraction -Extended Version[END_REF]. From different keyloggers written in C for Windows, we constructed abstract behaviors of keylogger features. Then, tests we ran on keyloggers to know whether we are able to detect information leaking were successful.

Another exemple comes from an Android application for cell-phone named SMS_Replicator_Secret, which forwards received SMS to the attacker. This application defines a class SMSReceiver with a particular method OnReceive (Context context, Intent intent). It then requests Android systems through its file metadata, to execute OnReceive on each SMS received or sent. We extracted from this application abstract behaviors corresponding to SMS leaks. Unlike the previous case study, we ran partial tests because of the difficulty to set up an Android platform. They were successful.

Conclusion

We presented an original approach for detecting high-level behaviors in programs, describing combinations of functionalities and defined by first-order temporal logic formulas. Behavior patterns, expressing concrete realizations of functionalities, are also defined by first-order temporal logic formulas. Abstraction of these functionalities in program traces is performed by term rewriting. Validation of the abstracted traces with respect to some high-level behavior is performed via usual model checking techniques. In order to address the general intractability of the problem of constructing the normal form trace set for a given program, we have identified a property of practical high-level behaviors allowing us to avoid computing normal forms and yielding a linear time detection algorithm.

Abstraction is a key notion of our approach. Providing an abstracted form for program traces and behaviors allows us to be independent of the program implementation and to handle similar behaviors in a generic way, making this framework robust with respect to variants. The fact that high-level behaviors are combinations of elementary patterns enables us to efficiently summarize and compact the possible combinations likely to compose suspicious behaviors. Moreover, high-level behaviors and behavior patterns are easy to update since they are expressed in terms of basic blocks.

Our approach is at an early stage. We think that the theoretical results on behavioral analysis presented here are promising. Applicability of our detection technique could be further enhanced by automating construction of reference behavior patterns, for example using mining techniques as in [START_REF] Christodorescu | Mining specifications of malicious behavior[END_REF].

  For instance, the term f open (1, 2) • f write (1, 3) represents the execution trace of a file open call f open (1, 2) followed by a file write call f write (1, 3), where 1 ∈ F d identifies the file handle returned by f open, 2 ∈ F d identifies the file path and 3 ∈ F d identifies the written data.

Definition 6 .

 6 Let C be a finite set of behavior patterns. An abstraction relation w.r.t C is the union of the abstraction relations w.r.t. the elements of C.

Theorem 4 .

 4 Let R be an abstraction relation such that R and R -1 are rational. Let τ be a tree transducer realizing R. Let M be a regular abstract behavior with the property of (m, n)-completeness and A M be a tree automaton recognizing the set of traces n-reliably realizing M w.r.t. R. Deciding whether a regular set of traces L, recognized by a tree automaton A, exhibits M takes O |τ | m•(m+1)/2 × |A| × |A M | time and space.

λ

  steal (x) := GetAsyncKeyState(x)∨ (RegisterDev(KBD, SINK) ⊙ GetInputData(x, INPUT)) ∨(∃y. SetW indowsHookEx(y, WH KEYBOARD LL)∧ ¬U nhookW indowsHookEx(y)U HookCalled(y, x)) ∨∃y.T elephonyM anager getDeviceId(x, y) -network send functionality: λ leak (x) := ∃y, z. sendto(z, x, y) ∨ ∃y, z. (connect (z, y) ∧ ¬close(z) U send(z, x)) ∨ ∃c, s. HttpU RLConnection getOutputStream(s, c)∧ ¬OutputStream close(s)U OutputStream write(s, x)overwriting or freeing:λ inval (x) := f ree(x) ∨ ∃y. sprintf 0 (x, y) ∨ GetInputData(x, INPUT) ∨ . . .dependences:λ depends (x, y) := sprintf 0 (x, y) ∨ ∃s. sprintf 1 (x, s, y) ∨ ∃sb. StringBuilder append(sb, y) ⊙ SB toString(x, sb) .

The honeypot of the Loria's High Security Lab: http://lhs.loria.fr

Acknowledgements. We would like to thank Stephan Merz for fruitful discussions on temporal logics.


Michel Bauer
email: michel.bauer@cea.fr

Raphael Chetrite
email: raphael.chetrite@unice.fr

AND FR ÉD Kurusch Ebrahimi-Fard
email: kurusch@icmat.es

Éric Patras
email: patras@math.unice.fr

TIME-ORDERING AND A GENERALIZED MAGNUS EXPANSION

Keywords:

Both the classical time-ordering and the Magnus expansion are well-known in the context of linear initial value problems. Motivated by the noncommutativity between time-ordering and time derivation, and related problems raised recently in statistical physics, we introduce a generalization of the Magnus expansion. Whereas the classical expansion computes the logarithm of the evolution operator of a linear differential equation, our generalization addresses the same problem, including however directly a non-trivial initial condition. As a by-product we recover a variant of the time ordering operation, known as T * -ordering. Eventually, placing our results in the general context of Rota-Baxter algebras permits us to present them in a more natural algebraic setting. It encompasses, for example, the case where one considers linear difference equations instead of linear differential equations.

Contents

Introduction 1 1. Time-ordering and the Magnus expansion 2 1.1. The T-ordering map 2 1.2. The Magnus expansion 4 2. T-ordering, T * -ordering and time derivations 5 2.1. T-ordering and time derivations 5 2.2. T * -ordering and the Magnus formula 6 3. Linear recursions in Rota-Baxter algebras 8 4. Example

Introduction

The time-ordered exponential Y (t) = Texp t 0 A(s)ds solves the first order linear differential equation: Ẏ (t) = Y (t)A(t), with initial value Y (0) = 1. It is complemented by the solution written as a proper exponential of Magnus' expansion, Y (t) = exp (Ω(A)(t)). Therefore time-ordering and Magnus' expansion are naturally related. Indeed, the function Ω(A)(t) is simply defined as the logarithm of the time-ordered exponential. It is characterized as the solution of a particular non-linear differential equation:

Ω(A)(t) = -ad Ω(A)
e -ad Ω(A) -1 (A)(t), and can be calculated recursively, which in turn is accompanied by formidable computational challenges due to intricate algebraic and combinatorial structures. Linear initial value problems are abundant in the mathematical sciences. And therefore the time-or T-ordering operation plays an essential role in many fields, for instance in quantum theory and statistical Date: June 18, 2012.

physics. In concrete applications one often needs to calculate time derivations of time-ordered products. However, the noncommutativity of the T-ordering operation and time derivation causes obstacles. Our work started out with the aim to understand a simple though surprising paradox caused by the aforementioned noncommutativity. It turns out that physicists introduced a variant of the time-ordering operation, denoted T * , which precisely encodes the lack of commutativity between the time-ordering prescription and time derivations. As part of this work we explore the relation between this modified time-ordering operation and the Magnus expansion (Theorem 1). This lead to a generalization of Magnus' result, allowing to include the initial value into the Magnus expansion (Theorem 2).

One may consider the time-ordered exponential as the formal solution of the linear integral equation:

Y (t) = Y 0 + t 0 Y (
s)A(s)ds corresponding to the initial value problem. It recently became clear [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF] that such integral equations, seen as linear fixpoint equations, are just a particular example of a more general class of abstract linear fixpoint equations: Y = 1 + R(AY ) defined in associative Rota-Baxter algebras (Theorem 5). We therefore embedded the generalized Magnus expansion into the context of such algebras, by showing in detail a theorem that specializes to the particular case (Theorem 7).

Let us remark that both time-ordering and Magnus' expansion have triggered much attention and progress in applied mathematics and physics. See for instance [START_REF] Blanes | Magnus expansion: mathematical study and physical applications[END_REF][START_REF] Iserles | Lie-group methods[END_REF][START_REF] Mielnik | Combinatorial approach to Baker-Campbell-Hausdorff exponents[END_REF][START_REF] Strichartz | The Campbell-Baker-Hausdorff-Dynkin formula and solutions of differential equations[END_REF][START_REF] Wilcox | Exponential operators and parameter differentiation in quantum physics[END_REF]. Recently, however, Magnus' work has also been explored successfully from a more algebraic-combinatorial perspective using operads, rooted trees, Hopf algebras, pre-Lie algebras, and the theory of noncommutative symmetric functions [START_REF] Chapoton | Enveloping algebras of preLie algebras, Solomon idempotents and the Magnus formula[END_REF][START_REF] Ebrahimi-Fard | The combinatorics of Bogoliubov's recursion in renormalisation, in 'Renormalization and Galois theories[END_REF][START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF][START_REF] Gelfand | Noncommutative symmetric functions[END_REF][START_REF] Murua | The Hopf algebra of rooted trees, free Lie algebras, and Lie series[END_REF].

Finally, as a word of warning, we should mention that we deliberately ignore any convergence issues. This work addresses mainly formal algebraic and related combinatorial aspects.

The paper is organized as follows. In the first section we introduce the objects we are going to consider in this work, i.e. the time-ordering map and the Magnus expansion. In section 2 we introduce a variant of the time-ordering operation, which reflects the non-commutativity of time-ordering and time derivation. The connection to the Magnus expansion is detailed. Section 3 recalls briefly the notion of Rota-Baxter algebras, and we then embed the foregoing results into this context. We also show a mild generalization of Atkinson's factorization theorem for Rota-Baxter algebras. The notion of R-center is introduced, which plays an important role. Finally, in section 4 we present finite differences as a simple example.

Time-ordering and the Magnus expansion

1.1. The T-ordering map. Linear initial value problems (IVP) play a major role in many parts of applied mathematics and theoretical physics. They consist of an ordinary linear differential equation for an unknown function Y (t):

d dt Y (t) = Y (t)A(t) (1)
together with a specified value of this function at a given point in time, e.g. say for t = 0, Y (0) = Y 0 , which we call the initial value. The functions Y (t) and A(t) being for instance matrix valued and differentiable.

Further simplifying the problem, e.g. by restricting to scalar valued functions, the solution of ( 1) is given straightforwardly in terms of the exponential map:

(2)

Y (t) = Y 0 exp t 0 A(s)ds .
Returning to the more challenging case, when noncommutativity prevails, we see that the result is far from simple. Recall that the formal solution of ( 1) is given by the series of iterated integrals:

(3)

Y (t) = Y 0 1 + t 0 A(s 1 )ds 1 + t 0 s 1 0 A(s 2 )ds 2 A(s 1 )ds 1 + • • • ,
where 1 would be the identity matrix in the context of matrix valued differentiable functions. The right hand side, known as Dyson-Chen or T(ime)-ordered series, follows forthrightly from the solution of the integral equation:

Y (t) = Y 0 + t 0 Y (s)A(s)ds (4)
corresponding to [START_REF] Aczél | Lectures on functional equations and their applications[END_REF]. Note that in the commutative case series (3) simply follows from expanding the exponential map (2) and making use of the integration by parts rule:

t 0 f (s)ds t 0 g(u)du = t 0 s 0 f (s)g(u)du ds + t 0 u 0 f (s)g(u)ds du. ( 5
)
Let us recall the notion of time-or T-ordering. Time ordering is defined in terms of the T-map:

T[U (s 1 )V (s 2 )] = U (s 1 )V (s 2 ), s 1 < s 2 V (s 2 )U (s 1 ), s 2 < s 1 .
Written more concisely it involves Heaviside step functions [START_REF] Fried | Green's Functions and Ordered Exponentials[END_REF]:

T[U (s 1 )V (s 2 )] := Θ(s 2 -s 1 )U (s 1 )V (s 2 ) + Θ(s 1 -s 2 )V (s 2 )U (s 1 ),
with a generalization to higher products of operators:

T[U 1 (s 1 ) • • • U n (s n )] := σ∈Sn Θ σ n U σ(1) (s σ(1) ) • • • U σ(n) (s σ(n) ),
where

Θ σ n := n i=1 Θ(s σ(1) -s σ(2) ) • • • Θ(s σ(n-1) -s σ(n) ). Observe that for any permutation σ ∈ S n , T[U 1 (s 1 ) • • • U n (s n )] = T[U σ(1) (s σ(1) ) • • • U σ(n) (s σ(n) )]
. Following the convention that the T-map operates before integration, the solution of the IVP (1) writes:

Y (t) = Y 0 Texp t 0 A(s)ds := Y 0 n≥0 1 n! t 0 • • • t 0 T[A(s 1 ) • • • A(s n )]ds 1 • • • ds n .
Each n-fold T-product inside the integral produces n! strictly iterated integrals, and therefore the series coincides with [START_REF] Atkinson | Some aspects of Baxter's functional equation[END_REF].

As a remark we would like to mention that our work started out with the aim to understand a simple though surprising paradox caused by the noncommutativity of the T-ordering operation and time derivation. See [START_REF] Bachmann | Time Ordering and Counting Statistics[END_REF] for an interesting example where this plays a decisive role, and [START_REF] Talkner | Fluctuation theorems: Work is not an observable[END_REF] for a case where this paradox caused some confusion. We assume nonnegative t, and A t := A(t) may be a finite-dimensional matrix valued function, or more generally a linear operator valued map. The following identity:

exp (A t -A 0 ) = exp t 0 du
dA u du may be considered as evident. However, its T-ordering cousin, which would result from a naive action of the T-ordering operation on both sides of the foregoing equation:

(6) Texp (A t -A 0 ) = Texp t 0 du dA u du
does not hold. Indeed, let us look at the second order term of each side separately:

T (A t -A 0 ) 2 = A 0 A 0 -2A 0 A t + A t A t ,
whereas:

T ( t 0 du dA u du ) 2 = t 0 du t u dv dA u du dA v dv + t 0 du u 0 dv dA v dv dA u du = 2 t 0 du t u dv dA u du dA v dv = 2 t 0 du dA u du (A t -A u ) = 2(A t -A 0 )A t -2 t 0 du dA u du A u .
Hence, we have verified that:

T (A t -A 0 ) 2 = T t 0 du dA u du 2 .
In fact, it is clear that [START_REF] Blanes | Magnus expansion: mathematical study and physical applications[END_REF] does not hold due to the lack of commutativity of the T-ordering with time derivation, which, on the other hand, is caused by the Heaviside step functions involved in the definition of the T-ordering map. However, observe that the difference reads:

T (A t -A 0 ) 2 -T t 0 du dA u du 2 = -A t A t + A 0 A 0 + 2 t 0 du dA u du A u = -A t A t + A 0 A 0 + t 0 du dA u du A u + A u dA u du + t 0 du dA u du A u -A u dA u du = -A t A t + A 0 A 0 + A t A t -A 0 A 0 + t 0 du dA u du A u -A u dA u du = t 0 du dA u du , A u .
In the sequel we will further remark on this observation, and explore in more detail the object, denoted Φ dAu du , such that the following equality holds:

(7) Texp (A t -A 0 ) = Texp t 0 du Φ dA u du .
1.2. The Magnus expansion. It is clear that the proper exponential solution of (1) changes drastically in the light of the noncommutative character of the problem. Wilhelm Magnus proposed in his seminal 1954 paper [START_REF] Magnus | On the exponential solution of differential equations for a linear operator[END_REF] a particular differential equation for the logarithm of the series (3) of iterated integrals (with initial value Y 0 = 1), which we denote by the function Ω(A)(t):

Ω(A)(t) = A(t) + n>0 (-1) n B n n! ad (n) t 0 Ω(A)(s)ds (A(s)) = -ad Ω(A) e -ad Ω(A) -1 (A)(t), with Ω(A)(0) = 0. The B n are the Bernoulli numbers B 0 = 1, B 1 = -1 2 , B 2 = 1 6 , . . . and B 2k+1 = 0 for k ≥ 1, such that the solution of the IVP (1) (with Y 0 = 1) is given by: (8) Y (t) = exp t 0 Ω(A)(s)ds .
Here, as usual, the n-fold iterated Lie bracket is denoted by ad

(n) a (b) := [a, [a, • • • [a, b]] • • • ]. Recall that: -z exp(-z) -1 = n≥0 (-1) n B n n! z n and exp(-z) -1 -z = 1 0 exp(-sz)ds.
The reader is encouraged to consult [START_REF] Blanes | Magnus expansion: mathematical study and physical applications[END_REF] for an authoritative review on the Magnus expansion and its ramifications. References [START_REF] Mielnik | Combinatorial approach to Baker-Campbell-Hausdorff exponents[END_REF][START_REF] Strichartz | The Campbell-Baker-Hausdorff-Dynkin formula and solutions of differential equations[END_REF][START_REF] Wilcox | Exponential operators and parameter differentiation in quantum physics[END_REF] are classical sources regarding Magnus' work. Let us write down the first few terms of what is called Magnus' series, Ω(λA)(s) = n≥1 λ n Ω n (A)(s), following from Picard iteration to solve the above recursion:

d dt Ω(λA)(t) = λA(t) + λ 2 1 2 t 0 A(s)ds, A(t) +λ 3 1 4 t 0 s 0 A(u)du, A(s) ds, A(t) + λ 3 1 12 t 0 A(s)ds, t 0 A(u)du, A(t) + • • • ,
where we introduced a parameter λ for later convenience. In the light of the IVP (1) and its two solutions, i.e. the proper exponential solution using Magnus' expansion, and the T-ordered exponential, we find the identity (for Y 0 = 1):

(9) Texp t 0 A(s)ds = exp t 0 Ω(A)(s)ds .
The terms beyond order one in Ω(λA)(s) = λ t 0 A(s)ds+ n≥2 λ n Ω n (A)(s) consist of iterated Lie brackets and integrals. For each n > 1 they solely serve to rewrite higher powers ( t 0 A(s)ds) n as strictly iterated integral of order n, modulo a factor n!. For instance, verify that:

1 2 t 0 A(s)ds 2 + 1 2 t 0 s 0 A(u)du, A(s) ds = t 0 s 0 A(u)du A(s)ds
We remark that recently, Magnus' work has been successfully explored from a more algebraic-combinatorial perspective using the theory of operads, rooted trees, pre-Lie algebras, Rota-Baxter algebras, and the theory of noncommutative symmetric functions [START_REF] Chapoton | Enveloping algebras of preLie algebras, Solomon idempotents and the Magnus formula[END_REF][START_REF] Ebrahimi-Fard | The combinatorics of Bogoliubov's recursion in renormalisation, in 'Renormalization and Galois theories[END_REF][START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF][START_REF] Gelfand | Noncommutative symmetric functions[END_REF][START_REF] Iserles | Lie-group methods[END_REF][START_REF] Murua | The Hopf algebra of rooted trees, free Lie algebras, and Lie series[END_REF].

T-ordering, T * -ordering and time derivations

2.1. T-ordering and time derivations. Let us return to the erroneous identity [START_REF] Blanes | Magnus expansion: mathematical study and physical applications[END_REF]. Recall that to simplify the presentation, we sometimes write A t for A(t).

Theorem 1. The solution Φ to the equation:

Texp (A t -A 0 ) = Texp t 0 du Φ dA u du is explicitly given by: (10) Φ dA u du := ∞ n=1 1 n! n-1 m=0 (-1) m C m n-1 (A u ) m dA u du (A u ) n-1-m = e -ad Au -1 -ad Au dA u du
Observe that if A u commutes with its derivation, dAu du , A u = 0, then, as expected equation ( 10) reduces to Φ dAu du = dAu du . In fact, equation [START_REF] Ebrahimi-Fard | Rota-Baxter algebras and new combinatorial identities Letters in[END_REF] On the other hand it is clear from its definition, that:

Texp (A t -A 0 ) = exp (-A 0 ) exp (A t ) .
Therefore:

d dt Texp (A t -A 0 ) = exp (-A 0 ) d dt exp (A t ) = exp (-A 0 ) exp (A t ) exp (-A t ) d dt exp (A t ) (11) = (Texp (A t -A 0 )) exp (-A t ) d dt exp (A t ) ,
which again shows that (6) can not be correct. However, the last equality may be used to derive [START_REF] Ebrahimi-Fard | Rota-Baxter algebras and new combinatorial identities Letters in[END_REF]. Indeed [START_REF] Ebrahimi-Fard | The combinatorics of Bogoliubov's recursion in renormalisation, in 'Renormalization and Galois theories[END_REF] implies:

Texp (A t -A 0 ) = Texp t 0 du exp (-A u ) d du exp (A u ) .
Using Duhamel's formula:

(12) exp (-A u ) d du exp (A u ) = 1 0 dν exp (-νA u ) dA u du exp (νA u ) ,
and recalling that:

1 0 dν exp(-νa)b exp(νa) = i≥1 (-1) i-1 i! ad (i-1) a (b) = e -ada -1 -ad a (b), yields: (13) exp (-A 0 ) exp (A t ) = T exp (A t -A 0 ) = Texp t 0 du e -ad Au -1 -ad Au dA u du .
This implies [START_REF] Ebrahimi-Fard | Rota-Baxter algebras and new combinatorial identities Letters in[END_REF] because ad 2.2. T * -ordering and the Magnus formula. Recall that the modified time-or T * -ordering is defined precisely so as to encode appropriately the lack of commutativity between the T-ordering and time derivations. In [START_REF] Bachmann | Time Ordering and Counting Statistics[END_REF] the interested reader can find motivations for the introduction of this particular variant of the time ordering operator coming from statistical physics, as well as further bibliographical references on the subject. For I(t) := dQ(t) dt , we define:

T * [I(t 1 ) • • • I(t n )] := ∂ ∂t n • • • ∂ ∂t 1 T[Q(t 1 ) • • • Q(t n )].
For any permutation σ ∈ S n :

T * [I(t 1 ) • • • I(t n )] = T * [I(t σ(1) ) • • • I(t σ(n) )],
or, equivalently, we have an invariance under the right action of the symmetric group, S n , in n elements, T * = T * • σ. In particular, because of this property, T * is entirely characterized by its action on time-ordered products

I(t 1 ) • • • I(t n ), t 1 ≤ ... ≤ t n , or, equivalently on products I(t 1 ) m 1 • • • I(t n ) mn , t 1 < • • • < t n .
Therefore we get, by setting I(t) = Ȧ(t) and Q(t) = A(t) -A(0):

T * exp t 0 du Ȧu = n 1 n! t 0 • • • t 0 n i=1 dt i ∂ ∂t n • • • ∂ ∂t 1 T (A(t 1 ) -A(0)) • • • (A(t n ) -A(0)) = n 1 n! T (A(t) -A(0)) • • • (A(t) -A(0)) = n k≤n 1 n! n k (-1) k A(0) k A(t) n-k = exp(-A(0)) exp(A(t)).
Equation ( 13) yields:

(14) T * exp t 0 du Ȧu = Texp t 0 du e -ad Au -1 -ad Au Ȧu .
Let us look at the degree two terms in A and Ȧ on both sides of this equality. We find:

1 2! t 0 t 0 T * [ Ȧu 1 Ȧu 2 ]du 1 du 2 = 1 2! t 0 t 0 T [ Ȧu 1 Ȧu 2 ]du 1 du 2 + 1 2! t 0 ad Au 1 ( Ȧu 1 )du 1 .
Simply rewriting the last term on the right hand side:

1 2! t 0 ad Au 1 ( Ȧu 1 )du 1 = 1 2! t 0 t 0 ad Au 1 ( Ȧu 2 )δ(u 1 -u 2 )du 1 du 2
we get finally, for u 1 different from u 2 :

T * [ Ȧu 1 Ȧu 2 ] = T [ Ȧu 1 Ȧu 2 ].
On the diagonal, i.e. for u 1 = u 2 we obtain:

T * [ Ȧu 1 Ȧu 2 ] = ad Au 1 ( Ȧu 2 )δ(u 1 -u 2 ).
In general, by identifying homogeneous components on each side of the foregoing equation, and taking into account the permutational invariance of T * (so that e.g.

T * [ Ȧu 1 Ȧu 2 Ȧu 1 ] = T * [ Ȧ2 u 1 Ȧu 2 ]
), we finally arrive at:

1 n! n n 1 , . . . , n k T * Ȧu 1 • • • Ȧun = T   (-1) n 1 ad (n 1 -1) Ac 1 n 1 ! ( Ȧc 1 ) • • • (-1) n k ad (n k -1) Ac k n k ! ( Ȧc k )   δ 1 • • • δ k , for arbitrary 0 ≤ c 1 < • • • < c k ≤ t, and n 1 , . . . , n k , such that n = n 1 + • • • + n k , u 1 = • • • = u n 1 = c 1 , . . . , u n 1 +•••+n k-1 +1 = • • • = u n 1 +•••+n k-1 +n k = c k .
Recall that the multinomial coefficient on the left hand side stands for n!(n

1 ! • • • n k !) -1 .
Here we wrote δ i for the product of delta functions δ(u

n 1 +•••+n i-1 +1 - u n 1 +•••+n i-1 +2 ) • • • δ(u n 1 +•••+n i-1 +n i -1 -u n 1 +•••+n i-1 +n i )
encoding the change from a n-dimensional integral to a k-dimensional integral from the left to the right hand side of equation [START_REF] Ebrahimi-Fard | A noncommutative Bohnenblust-Spitzer identity for Rota-Baxter algebras solves Bogoliubov's recursion[END_REF]. Note that we have recovered [4, eq. 2.11] (up to signs, due to different conventions regarding time-orderings):

Corollary 3. We have, with our previous notation:

(15) T * [ Ȧu 1 • • • Ȧun ] = (-1) n T[ad (n 1 -1) Ac 1 ( Ȧc 1 ) • • • ad (n k -1) Ac k ( Ȧc k )]δ 1 • • • δ k

Linear recursions in Rota-Baxter algebras

We take now a broader perspective on linear IVP by replacing (4) in terms of general linear operator fixpoint equations. A natural setting to do so is provided by associative Rota-Baxter k-algebra, which we briefly recall in this section. For more details we refer the reader to [START_REF] Atkinson | Some aspects of Baxter's functional equation[END_REF][START_REF] Baxter | An analytic problem whose solution follows from a simple algebraic identity[END_REF][START_REF] Ebrahimi-Fard | Rota-Baxter algebras and new combinatorial identities Letters in[END_REF][START_REF] Ebrahimi-Fard | A noncommutative Bohnenblust-Spitzer identity for Rota-Baxter algebras solves Bogoliubov's recursion[END_REF][START_REF] Rota | Fluctuation theory and Baxter algebras[END_REF] and references therein. See also [START_REF] Aczél | Lectures on functional equations and their applications[END_REF][START_REF] Aczél | Functional Equations in Several Variables: With Applications to Mathematics, Information Theory and to the Natural and Social Sciences, Encyclopedia of Mathematics and its Applications[END_REF] for interesting aspects. We assume the underlying base field k to be of characteristic zero, e.g. k = R or C.

Motivated by Frank Spitzer's seminal work [START_REF] Spitzer | A combinatorial lemma and its application to probability theory[END_REF] in probability theory, the mathematician G. Baxter [START_REF] Baxter | An analytic problem whose solution follows from a simple algebraic identity[END_REF], soon after followed by J. F. C. Kingman, W. Vogel, F. Atkinson, P. Cartier, Gian-Carlo Rota and others [START_REF] Atkinson | Some aspects of Baxter's functional equation[END_REF][START_REF] Cartier | On the structure of free Baxter algebras[END_REF][START_REF] Kingman | Spitzer's Identity and its use in Probability Theory[END_REF][START_REF] Vogel | Die kombinatorische Lösung einer Operator-Gleichung[END_REF][START_REF] Rota | Baxter algebras and combinatorial identities I, II[END_REF][START_REF] Rota | Ten mathematics problems I will never solve[END_REF][START_REF] Rota | Fluctuation theory and Baxter algebras[END_REF], explored a more general approach to the above linear IVP (1) and the corresponding linear integral equation ( 4

(17) R(x)R(y) = R(R(x)y + xR(y)) + θR(xy).
We call A a commutative Rota-Baxter k-algebra of weight θ ∈ k with unit 1. Observe that the map R := -θid -R is also a Rota-Baxter map of weight θ. Moreover, from identity [START_REF] Iserles | Lie-group methods[END_REF] it follows that the images of R and R are subalgebras in A.

Baxter gave a solution for ( 16) by proving Spitzer's classical identity in a commutative unital Rota-Baxter k-algebra of weight θ ∈ k, that is, he showed that the formal solution of ( 16) is given by:

(18) Y = 1 + ∞ n=1 R R(• • • R(R n-times (a)a)a • • • )a = exp -R log(1 -θa) θ .
Remark 4. Note that besides (16), Baxter, Atkinson and Vogel considered more general linear fixpoint equations and their solutions in a commutative Rota-Baxter k-algebra A. In [START_REF] Atkinson | Some aspects of Baxter's functional equation[END_REF][START_REF] Baxter | An analytic problem whose solution follows from a simple algebraic identity[END_REF] the equations E = a + λR(bE), F = R(a) + λR(bF ), with analog equations for R, and G = a + λR(bG) + λ R(cG) are solved for a, b, c ∈ A. In [START_REF] Vogel | Die kombinatorische Lösung einer Operator-Gleichung[END_REF] Vogel considered the equation H = a + λbR(H) + cλ R(H), and gave a solution for a, b, c ∈ A. The generalization of these equations and their solutions to non-commutative Rota-Baxter algebra was given in [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF][START_REF] Ebrahimi-Fard | Dendriform Equations[END_REF].

Let us return to [START_REF] Iserles | Lie-group methods[END_REF], which one may think of as a generalized integration by parts identity. Indeed, the Riemann integral, which satisfies the usual integration by parts rule [START_REF] Baxter | An analytic problem whose solution follows from a simple algebraic identity[END_REF], corresponds to a Rota-Baxter operator of weight zero. Observe that in the limit θ → 0 we obtain:

1 θ log(1 -θa) = - n>0 θ n-1 a n n θ→0 ------→ -a.
The right hand side of the last equality in [START_REF] Kingman | Spitzer's Identity and its use in Probability Theory[END_REF] reduces to the simple exponential solution Y = exp(R(a)).

In the context of the Riemann integral, this corresponds to the classical case (2) of the IVP (1), with

Y 0 = 1.
The extra term on the right hand side of (17) becomes necessary, for instance, when we replace the Riemann integral by a Riemann-type summation operator:

(19) S(f )(x) := n>0 f (x + n)
on a suitable class of functions. Indeed, one verifies that the map S satisfies the weight θ = 1 Rota-Baxter relation: S(f )S(g) = S S(f ) g + S f S(g) + S f g . More generally for finite Riemann sums:

R θ (f )(x) := [x/θ]-1 n=0 θf (nθ). ( 20
)
we find that R θ satisfies the weight θ Rota-Baxter relation:

R θ (f )R θ (g)(x) = R θ R θ (f )g (x) + R θ f R θ (g) (x) + θR θ (f g)(x).
Beside fluctuation theory in probability the Rota-Baxter relation recently played a crucial role in Connes-Kreimer's Hopf algebraic approach to perturbative renormalization [START_REF] Connes | Renormalization in quantum field theory and the Riemann-Hilbert problem I: The Hopf algebra structure of graphs and the main theorem[END_REF]. Here, Rota-Baxter algebras enter through projectors, which satisfy [START_REF] Iserles | Lie-group methods[END_REF]

for θ = -1. A paradigm is provided by the algebra A = C[ε -1 , ε]] = ε -1 C[ε -1 ] ⊕ C[[ε]] of Laurent series ∞
n=-k a n ε n (with finite pole part). The projector, called minimal subtraction scheme map, used in renormalization is defined by keeping the pole part:

R ms ∞ n=-k a n ε n = R ms -1 n=-k a n ε n + ∞ n=0 a n ε n := -1 n=-k a n ε n .
It is a Rota-Baxter map of weight θ = -1. In general, assume the k-algebra A decomposes, A = A 1 ⊕A 2 , and let R :

A → A be defined by R(a 1 , a 2 ) = a 1 , then R 2 = R. Hence: R(a)b + aR(b) -ab = R(a)R(b) -(id -R)(a)(id -R)(b) such that applying R yields R R(a)b + aR(b) -ab = R(a)R(b).
We refer the reader to [START_REF] Ebrahimi-Fard | A noncommutative Bohnenblust-Spitzer identity for Rota-Baxter algebras solves Bogoliubov's recursion[END_REF] for more details including examples and applications.

In [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF][START_REF] Ebrahimi-Fard | Dendriform Equations[END_REF] the Spitzer identity has been generalized to non-commutative Rota-Baxter algebras: Remark 6. Observe that the right multiplication r θΩ ′ map accounts for the extra term in [START_REF] Iserles | Lie-group methods[END_REF]. Let us emphasize that in [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF] we formulated this theorem using the generic pre-Lie algebra structure underlying any associative Rota-Baxter algebra. Indeed, the above generalized adjoint operation,

(21) Ω ′ (λa) = -ad R(Ω ′ ) + r θΩ ′ e -ad R(Ω ′ ) +r θΩ ′ -1 (λa) = m≥0 (-1) m B m m! ad (m)
ad a (b) = ad R(a) (b) -r θa (b) = [R(a)
, b]θba, defines a pre-Lie product on A. However, we refrain from using the pre-Lie picture for reasons to become clear in the sequel.

We introduce now the notion of the R-center in a Rota-Baxter algebra A of weight θ, defined as the following subset of elements in A:

Z R (A) := {x ∈ A | xR(a) = R(xa) and R(a)x = R(ax), ∀a ∈ A}.
Observe that the R-center forms a subalgebra of A. Indeed, for u, v ∈ Z R (A), we have uvR(a) = uR(va) = R(uva), and [R(a), x] = R([a, x]). Notice the identity R(x) = xR(1), for any x ∈ Z R (A). In the context of matrix valued differentiable function with the Riemann integral as weight zero Rota-Baxter map, the R-center includes amongst others the constant matrices. Another useful example are upper (or lower) triangular matrices, say, with unit diagonal, and entries in an arbitrary Rota-Baxter algebra A of weight θ. They form a noncommutative Rota-Baxter algebra M A of weight θ with the natural Rota-Baxter map. In this case the triangular matrices with entries strictly in k are in the R-center. Now we would like to prove that the combinatorial structure underlying the T * -operation, that is the solution of the IVP provided by Theorem 2, extends to Rota-Baxter algebras.

Theorem 7. Let (A, R) be a unital Rota-Baxter k-algebra of weight θ ∈ k. Let α be an element in its R-center, and Ω ′ α := Ω ′ α (λa), a ∈ A, be the element of A[[λ]] such that:

X = exp α + R(Ω ′ α )
, where X is the solution of the linear fixpoint equation:

X = exp(α) + λR(Xa).
The element Ω ′ α obeys the following recursive equation:

(22) Ω ′ α (λa) = -ad α+R(Ω ′ α ) + r θΩ ′ α e -ad α+R(Ω ′ α ) +r θΩ ′ α -1 (λa) = m≥0 (-1) m B m m! ad (m) α,Ω ′ α (λa),
where ad α,Ω ′ α (b) := ad α+R(Ω ′ α )r θΩ ′ α . Observe that this theorem is a generalization of Theorems 2 and 5. Returning to Remark 6, we see here that this generalization involves the operation ad a,b := ad a+R(b) -r θb , which does not define a pre-Lie algebra product on the Rota-Baxter k-algebra A.

Proof. We follow partly [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF]. First, note that we can decompose ad α+R(

Ω ′ α ) = ℓ α+R(Ω ′ α ) -r α+R(Ω ′ α )
, where ℓ a (b) := ab. It is clear that both operations commute, that is, ℓ a r b (c) = acb = r b ℓ a (c). Now, let:

λa = e -ad α+R(Ω ′ α ) +r θΩ ′ α -1 -ad α+R(Ω ′ α ) + r θΩ ′ α (Ω ′ α ) = 1 0 dse -s(ad α+R(Ω ′ α ) -r θΩ ′ α ) (Ω ′ α ) = 1 0 dse -s(ℓ α+R(Ω ′ α ) -r α+R(Ω ′ α ) -r θΩ ′ α ) (Ω ′ α ) = 1 0 dse -sℓ α+R(Ω ′ α ) e sr α+R(Ω ′ α ) +sr θΩ ′ α (Ω ′ α ).
Now, we multiply by X = exp α + R(Ω ′ α ) from the left:

Xa = 1 0 dse (1-s)ℓ α+R(Ω ′ α ) e s(r α+R(Ω ′ α ) +r θΩ ′ α ) (Ω ′ α ) = 1 0 ds p,q≥0 (1 -s) p s q q!p! (ℓ α+R(Ω ′ α ) ) p (r α+R(Ω ′ α ) + r θΩ ′ α ) q (Ω ′ α ) = 1 0 ds p,q≥0 (1 -s) p s q q!p! (ℓ α+R(Ω ′ α ) ) p (r α+R(Ω ′ α )+θΩ ′ α ) q (Ω ′ α ) = n>0 1 n! p+q=n-1 (α + R(Ω ′ α )) p (Ω ′ α )(α -R(Ω ′ α )) q ,
where we used that -R = θid+R. Hence, we would like to show that X -exp(α) = λR(Xa). Expanding:

X -exp(α) = n≥0 1 n! (α + R(Ω ′ α )) n -α n ,
lefts us with the goal to prove order by order the general identity:

n>0 1 n! (α + R(β)) n -α n = n>0 1 n! p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q ,
where α ∈ Z R (A) and β is an arbitary element in A.

The case n = 1 is obviously true. Let us look at n = 2. Then we have on the left hand side:

(α + R(β)) 2 -α 2 = αR(β) + R(β)α + R(β)R(β) = R(αβ) + R(βα) + R(β)R(β).
In the last line we used that α is in the R-center Z R (A). On the right hand side we find:

R (α + R(β))β + β(α -R(β)) = R αβ + R(β)β + βα + βR(β) + θββ = R(αβ + βα) + R(β)R(β).
In the last line we used the Rota-Baxter relation [START_REF] Iserles | Lie-group methods[END_REF]. We show now the case n + 1, assuming the identity holds up to order n. This yields:

(α + R(β)) n+1 -α n+1 = (α + R(β)) n (α + R(β)) -α n α = (α + R(β)) n R(β) + ((α + R(β)) n -α n )α = p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q R(β) + α n R(β) + p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q α = p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q R(β) + p+q=n-1 R R((α + R(β)) p (β)(α -R(β)) q β) + p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q θβ +R(α n β) + p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q α = p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q+1 + p+q=n-1 R R((α + R(β)) p (β)(α -R(β)) q )β + R(α n β) = p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q+1 +R (α + R(β)) n β -α n β + R(α n β) = p+q=n-1 R (α + R(β)) p (β)(α -R(β)) q+1 + R (α + R(β)) n β = p+q=n R (α + R(β)) p (β)(α -R(β)) q
where we recall that α -R(β) = α + θβ + R(β).

Note that in the context of the weight zero RB algebra defined in terms of the Riemann integral, the generalization following from the theorem allows to absorb the initial value in (1) directly into the Magnus' expansion. Remark 8. Recall Remark 4 and the fact that any Rota-Baxter algebra has two Rota-Baxter operators, R and R. In [START_REF] Atkinson | Some aspects of Baxter's functional equation[END_REF][START_REF] Baxter | An analytic problem whose solution follows from a simple algebraic identity[END_REF] Baxter and Atkinson showed that the solution to the recursions: E = a + λR(bE) and F = R(a) + λR(bF ) are given by F = R(aX)Y and E = a + R(abX)Y , respectively, where X, Y are solutions to:

X = 1 + λR(Xb) resp. Y = 1 + λ R(bY ).
Together with the solutions X and Y for the last two fixpoint equations comes the so-called Atkinson factorization, which generalizes straightforwardly in the context of the above theorem.

Example: Finite differences

As an example of an interesting fixpoint equation involving a non-zero weight Rota-Baxter structure, we will now approach the particular case of a linear finite difference initial value problem. For this, we define the finite time-difference operator ∆ such that for all functions f defined on N:

∆(f )(n) := f (n + 1) -f (n).
Observe that this map satisfies a generalized Leibniz rule:

∆(f g)(n) = (f g)(n + 1) -(f g)(n) = f (n + 1)g(n + 1) -f (n)g(n) = f (n)∆(g)(n) + ∆(f )(n)g(n) + ∆(f )(n)∆(g)(n)
Recall the finite Riemann sum map [START_REF] Mielnik | Combinatorial approach to Baker-Campbell-Hausdorff exponents[END_REF], R(X) n := follows when we note that 1 + exp (-A k ) ∆ [exp (A k )] = exp (-A k ) exp (A k+1 ) . Then, we first apply Duhamel's formula [START_REF] Spitzer | A combinatorial lemma and its application to probability theory[END_REF], and second expand exp (-νA k ) and exp (νA k+1 ) , and eventually we do the explicit integration of ν. This yields:

(26) exp (-A 0 ) exp (A N ) = --→

N -1 k=0 1 + ∞ N =1 1 N ! N -1 n=0 (-1) n C n N -1 (A k ) n ∆ [A k ] (A k+1 ) N -1-n .
Finally, we note that:

N -1 n=0 (-1) N -1-n C n N -1 (A k ) n ∆ [A k ] (A k+1 ) N -1-n = l A k -r A k+1 N -1 ∆ [A k ] ,
such that:

∞ N =1 1 N ! N -1 n=0 (-1) n C n N -1 (A k ) n ∆ [A k ] (A k+1 ) N -1-n = ∞ N =1 (-1) N -1 N ! l A k -r A k+1 N -1 ∆ [A k ] = exp -l A k + r A k+1 -Id -l A k + r A k+1 ∆ [A k ] .
This relation, together with (26) concludes the proof of ( 24).

a

  (b) = m-n n=0 (-1) n C n m a n ba m-n .Conversely, if we set B t := Φ dAu du and X t := exp(A t ), we arrive at the following first generalization of the classical result of Magnus[START_REF] Chapoton | Enveloping algebras of preLie algebras, Solomon idempotents and the Magnus formula[END_REF].

Theorem 2 .

 2 The IVP: Ẋt = X t B t , X 0 = exp(α) is solved by:X t = exp α + t 0 Ωα (B)(s)ds , with: Ωα (B)(u) := -ad α+ u 0 Ωα(B)(s)ds e -ad α+ u 0 Ωα(B)(s)ds -1 (B(u)).

  ) -in the case of Y 0 = 1 -, by suggesting to work with the linear fixpoint equation: (16) Y = 1 + λR(Y a), in a commutative unital k-algebra A, a ∈ A, respectively the filtered and complete algebra A[[λ]]. The linear map R on A is supposed to satisfy the Rota-Baxter relation of scalar weight θ ∈ k:

Theorem 5 .

 5 [START_REF] Ebrahimi-Fard | A Magnus-and Fer-type formula in dendriform algebras[END_REF] Let (A, R) be a unital Rota-Baxter k-algebra of weight θ ∈ k. Let Ω ′ := Ω ′ (λa), a ∈ A, be the element of λA[[λ]] such that:Y = exp R(Ω ′ ), where Y = Y (a) is the solution of the linear fixpoint equation Y = 1 + λR(Y a). This element obeys the following recursive equation:

Ω

  ′ (λa) with B l the Bernoulli numbers, r θa (b) := θba, and ad a (b) := ad R(a) (b)r θa (b).

Proposition 9 .

 9 Let (A, R) be a unital Rota-Baxter k-algebra of weight θ ∈ k. Let α, β be in its R-center Z R (A). Then we have a factorization:1λa = X -1 exp(γ)Y -1 ,where: X = exp(α) + λR(Xa) Y = exp(β) + λ R(aY ), and exp(γ) = exp(α) exp(β), γ ∈ Z R (A).

Proof.

  The proof reduces to a simple verification.XY = exp(γ) + λR(Xa) exp(β) + λ exp(α) R(aY ) + λ 2 R(Xa) R(aY ) = exp(γ) + λR(Xa exp(β)) + λ R(exp(α)aY ) + λ 2 R(Xa) R(aY ) = exp(γ) + λR Xa(exp(β) + λ R(aY )) + λ R (exp(α) + λR(Xa))aY = exp(γ) + λXaY,from which the result follows.

n- 1 k=0X

 1 k . The latter satisfies the Rota-Baxter relation of weight θ. We put the weight equal to one, R := R 1 . Then:

  follows from exploring briefly what went wrong in the first place with identity[START_REF] Blanes | Magnus expansion: mathematical study and physical applications[END_REF]. Indeed, recall that X t = Texp t 0 duB u for a family of operator valued maps B t is the solution to the simple IVP d dt X t = X t B t , X 0 = 1.

			Hence:
	d dt	Texp	0	t	du	dA u du	= Texp	0	t	du	dA u du	dA t dt	.

Acknowledgements The third author is supported by a Ramón y Cajal research grant from the Spanish government. We thank D. Manchon for helpful discussions. We thank the CNRS (GDR Renormalisation) for support.

= f (m)f (0). We are interested in the finite difference initial value problem: [START_REF] Rota | Ten mathematics problems I will never solve[END_REF] ∆X n = X n B n X 0 = exp (A 0 ) where X n := X(n) and B n = -1. Applying R leads to a generalized Atkinson equation:

which yields:

Observe that the solution can be written as a finite product, as well as, using Theorem 5, as an exponential:

Now, by applying Theorem 7, with α = A(0) and Ω ′ α = ∆A (recall that X = exp(A) and R(∆A) = A -A(0)), we get: Theorem 10. With our previous notation, for the finite difference IVP [START_REF] Rota | Ten mathematics problems I will never solve[END_REF] we get:

where as before ℓ X is the left multiplication by X and r X is the right multiplication by X.

In particular:

Note that these formulas can also be obtained from a straightforward calculation. We include a direct proof for the sake of transparency. The starting point is a discrete analog of Duhamel's formula (12): Lemma 11. We have:

The proof follows by taking the integral from 0 to 1 of the following equality:

Now we verify identity [START_REF] Rota | Fluctuation theory and Baxter algebras[END_REF]. The first thing to remark is that: