#!/bin/blog --author=p4bl0

the blog where all numbers are written in base 10

λ-virus

by p4bl0, on
last update by p4bl0, on

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 TV 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, (TV 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 TV 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 TV) is simply IdV. 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
If you have any remark about this blog or if you want to react to this article feel free to send me an email at "pablo <r@uzy dot me>".