🚀 go-pugleaf

Stefano_Turci@f0.n462.z9.virnet.bad.se (Stefano Turci) writes:
>  I run it on a high number of files infected with two Mte-based viruses
>  ( Dedicated and Pogue) and it is able to detect all of the infected
>  files, but how could I say if it will work for *EVERY* mutation and
>  for *EVERY* Mte-based virus ?
>  I think it's impossible.

On 04 Nov 92 11:27:52 +0000 Vesselin Bontchev
<bontchev@fbihh.informatik.uni-hamburg.de> said:
> You are right, it's impossible. That's why, our tests can only prove
> that a scanner is NOT able to detect the MtE-based viruses reliably.
> Otherwise we can only say that we have been unable to find an MtE
> replicant that the scanner does not detect.

Just to prevent a possible misunderstanding of Stefano's and
Vesselin's claim:

It is indeed impossible to tell it from tests alone, without
considering the program's internal algorithms.

However, it is probably possible (however difficult it may be) to
prove that an Mte detector is reliable: The proof would be based on
the following steps: 
1. Infer, from a sample of the MtE, the algorithm used to produce the
   various decryptors, and prove that the algorithm found and the MtE
   sample are indeed equivalent;
2. infer from that algorithm the set of all decryptors that can possibly
   be produced from the MtE (of course not as a huge list of detailed
   code sections, but rather as a comparably moderate list of possible
   features, or patterns), and prove that the set is indeed produced by
   the algorithm,
3. design an algorithm to detect all of these decryptors, reliably, and
   prove that it indeed does so.

Step 1, called reverse engineering, is routinely performed by many
virus researchers (though, maybe, without formal correctness proofs).

On step 3, read "A Discipline of Programming" by Edsger W. Dijkstra.
The basic idea of this book is to design a suitable proof first, then
write the program in accordance with that proof. This is recommended
reading for all would-be programmers!

Step 2 is probably the most difficult one, as it cannot rely on
established formal methods. Yet, it can probably be done -- as Rubik's
Cube, and many more seemingly intractable problems, have been solved,
eventually.

In principle (but not practically) it could even been done by an exhaust-
ive enumeration, as the set of all possibly produced code sections is
finite (There are two easy proofs for this finiteness. Outline proof 1:
The set of all starting states for the algorithm is finite, and the
algorithm is deterministic, hence it cannot produce more different
results than it has starting states. Outline proof 2: The length of the
produced code sections is limited by the size of the largest disk avail-
able, hence finite, hence the set of all possible code sections is the
power set of a finite set, which is still finite -- and the MtE will only
produce a small :-) subset of that power set.)

Best wishes,
                    Otto Stolz <RZOTTO@DKNKURZ1.Bitnet>
                               <RZOTTO@nyx.uni-konstanz.de>