λ-virus
What is a λ-virus? It's a virus in the
λ-calculus!
The idea comes from a question asked to
David Naccache by one of his
former students. They were talking about our
IMACC
article, Can a Program
Reverse-Engineer Itself?
. In which we define a notion of equivalence
between a function and an obfuscated version of it, and then show a
construction to protect functions from obfuscation (i.e., we can retreive
their original code and also repair them in the environment). The student
asked if the construction used by oximoron (the implementation of
the article) could be a protection against a λ-virus. Pr. Naccache
then asked Antoine and me our opinion about
this idea.
The first thing to do was to define what a λ-virus would actually be. I came up with an informal but satisfactory definition of what is an infected (i.e., contaminated and contagious) λ-term for a given λ-virus. If T is a λ-term then we call T_{V} the λ-term "T infected by the λ-virus V":
- If T is a λ-abstraction (which we can see as a function or a program), then for any λ-term E, (T_{V} E) is (T E)_{V}.
- If T isn't a λ-abstraction (we can see it as some data, e.g., the final result of a computation), then T_{V} is the value of (V* T), where V* is an arbitrary λ-abstraction defined by the creator of V.
The first point, for λ-abstraction, defines how the virus propagates. The second one defines how it acts. For instance we can imagine a virus which propagates until it infects a function which returns an integer and make this function always return 4.
At this stage we can already say that oximoron doesn't protect against this kind of attacks (it wasn't supposed to, but it would have been cool if it did). But let's forget about that, the idea of a λ-virus is fun enough in itself.
One thing we can remark with our definition of λ-virus is that the original form of a virus V, the λ-term whose only feature is to inoculate the virus to other λ-terms (i.e., Ṽ such that for any λ-term T, (Ṽ T) is T_{V}) is simply Id_{V}. I know it is obvious but I find that quite beautiful at the same time.
At first I tought that I would need to use a quine-based construction to create the virus, as we did in Pastis and oximoron. It would be true if the implementation was actually in λ-calculus, or at least working with S-expressions as oximoron does. But we can actually implement this notion of virus very easily in any language which has closure (pun intended). I did it in Scheme (Racket) and I implemented the possibility of adding side effects when the virus propagates:
(define (create-virus side-effect tweak) (define (infect target) (if (procedure? target) (lambda args (side-effect target) (infect (apply target args))) (tweak target))) (infect (lambda (x) x)))
The two arguments of create-virus
have to be functions. The
first one is for the side effects the virus creator might want to add. The
second one is the function the virus should apply to results (the V*
from earlier).
(create-virus (lambda (x) null) identity) ;; will propagate but won't do anything at all
(define tatltuae (create-virus (lambda (x) (displayln "Infected!")) (lambda (x) (if (number? x) 42 x)))) ;; will propagate, systematically print "Infected!" on ;; the current output port and replace any integral ;; return value by 42
> (define addn (tatltuae (lambda (n) (lambda (x) (+ n x))))) Infected! > (define add13 (addn 13)) Infected! > (add13 38) ;; should return 51 Infected! 42