1
$\begingroup$

Assume that I have a program Login.c that I have compiled with cc and generated the executable a.out. Now, along the questions posed from "Reflections of Trusting Trust", I want to check that a.out is the intended executable and nothing else, e.g. that there is no malfunction injected by the build system. There are techniques such as diverse double-compiling and reproducible builds that I can utilize. However, I see in several texts that say "

comparing source code and compiled code for equivalence is an undeciable problem

and, similarly, "This is an undecidable problem in general" but: Where is the reference or proof that this problem is undecidable?

$\endgroup$
8
  • $\begingroup$ Have you taken a course in computer science that explains undecidability? Have you heard of the halting problem? $\endgroup$
    – John L.
    Aug 27, 2022 at 11:16
  • $\begingroup$ @JohnL. Yes my major was theoretical computer science. I studied Karp reduction among other topics. But I've never seen a reduction from proving functional equivalence to the Halting problem, if that would be a proof. $\endgroup$ Aug 27, 2022 at 12:20
  • $\begingroup$ stackoverflow.com/questions/1132051/… @JohnL. Is it the same problem? $\endgroup$ Aug 27, 2022 at 12:21
  • $\begingroup$ It is a matter of trust $\endgroup$
    – kelalaka
    Aug 27, 2022 at 12:23
  • $\begingroup$ But I mean if I check bit-for-bit and they're identical then they are equivalent. $\endgroup$ Aug 27, 2022 at 12:23

1 Answer 1

1
$\begingroup$

"Comparing source code and compiled code for equivalence is an undecidable problem". What does that statement mean?

It means there is no algorithm that, given arbitrary (source) code in programming language $A$ and arbitrary (compiled) code in another programming language $B$, can decide whether both code always behave the same if given the same input. Here we assume both programming languages are arbitrarily fixed and Turing-complete. "behave the same" means either both loop forever or both return the same string.


Here is a simple proof.

Suppose there is such an algorithm $M$. Let us solve the halting problem in language $A$ using $M$.

Let $S_A$ be some arbitrary source code in $A$ and $w$ be some arbitrary string.

Since $B$ is Turing complete, we can write $S_B$, a program in $B$ that behaves the same as $S_A$.

Write code $S'_B$ in language $B$ so that it is the same as $S_B$ except when it halts. At the time when it halts before returning the result, it will check whether the given input is $w$ first. If it is, $S'_B$ will loop forever. Otherwise, it will return the result as usual. That is, $S'_B$ is the same as $S_B$ except possibly that $S'_B$ always loop forever if the input is $w$.

Now we use $M$ to check whether $S_A$ and $S'_B$ always behave the same if given the same input.

If $M$'s verdict is yes, then $S_A$ on $w$ does not halt. Otherwise, $S_A$ on $w$ halts. We have solved the halting problem in language $A$.

However, it is known that the halting problem in a Turing-complete language is undecidable. This contradiction implies that $M$ does not exist.


In fact, any nontrivial behavior property of a program in a Turing-complete language is undecidable. That is Rice's theorem.

What are the nontrivial behavior properties?

A property of a program is a behavior property if for any two programs that behaves the same, either both has that property or neither does.

A behavior property is nontrivial if at least one program has it while at least one program does not.

Here are some nontrivial behavior properties.
Will the program output "Niklas" if it runs without any input?
Is there an input that the program does not return the string as specified in a specification?
Will the program make a internet connection, assuming the program is allowed to?

$\endgroup$
1
  • $\begingroup$ "Behave the same" could be written as "function the same". $\endgroup$
    – John L.
    Aug 27, 2022 at 14:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.