In static program analysis, one of the most difficult parts of designing
analyzers is the join and widening algorithms. These algorithms are
used to approximate abstract states at control-flow join points. The
difficulty in their design stems from the fact that they are necessarily
heuristic: they must abstract enough for the analysis to be efficient
and feasible but must also be precise enough to capture the properties
of interest. Widenings are particularly "magical" as they are
essentially used to "guess" inductive invariants after a few iterations
of symbolically executing loops. The heuristics are typically based on
the forms of the input invariants.
As humans, we typically try to understand code by observing a few test
cases and then perhaps "guess" invariants by generalizing the observed
test cases. Could concrete traces be used as the basis for or to
provide useful for information to a join/widening algorithm? There are
at least two key challenges here: 1) how do we connect a dynamic trace
to the program text and a static analysis' representation of program
state?; 2) what kind of information would such concrete instances
provide a join/widening algorithm?
One possible "challenge example" is one that requires list invariants
that require a relation with the length of the list:
l = null;
for (i = 0; i < n; i++) {
// cons new node onto l
}
cur = l;
for (i = 0; i < n; i++) {
// do something with cur
cur = cur.next;
}
Amer brought up some potentially related work by Andrew Appel, and Aaron
also mentioned some work by Mike Ernst (Daikon). Aaron brought up a
good domain may be hash tables. It seems very difficult to do anything
with hash tables in a purely static setting.
High-level concurrent/parallel programming languages (e.g., CML, Erlang, Scala, Haskell) tend to offer one or a few high level synchronization constructs (e.g., synchronous or asynchronous message passing, I/M-variables) and then provide a library implementing other constructs in terms of the given ones. But these other secondary constructs are not as efficient as they could be. Thus, there is an imbalance in efficiency across the offered constructs. This imbalance begs the question: what is a "universal" language-level construct that would allow implementing all high-level constructs "efficiently" in libraries -- i.e., with only a constant overhead in space and time, no extraneous sleep/wake/sleep cycles, and no required blocking?
We're currently looking at a memory cell that implements compare-and-swap-like methods and get/set, where get is blocking under certain conditions and set broadcasts to all waiting threads. Such a cell can be efficiently implemented in the runtime using a lock-free stack, and it has no memory overhead when there is at most one waiting thread (which often arises when implementing other synchronization constructs).
Amer asked for an example, which I didn't explain well at the time. So here it is: consider implementing asynchronous message passing in Concurrent ML, which is based on synchronous message passing. The runtime already has queues for the blocking send and receive operations. Yet implementing asynchronous MP requires an additional user-level queue as well.
Later, I also remembered another advantage of a low-level construct: expressiveness. Reppy proved that any language with N-way synchronous communication (a meeting of N threads) is not sufficiently expressive to implement (N+1)-way synchronous communication. However, the memory cell allows implementing a library that can create N-way synchronous communication for arbitrary N.
Jeremy brought up the push vs. pull models of programming with their various trade-offs.
Compilers and program transformation tools are often limited in how drastically they can change a program because changing the order of evaluation may change the meaning of the program (i.e., may break the program). But what if the programming language did not specify a fixed evaluation order in the first place? In some sense, the compiler would be free to choose any order of evaluation (and to even parallelize the program). Of course, such a language would be quite difficult to program in, as the programmer would need to worry about data races showing up all over the place. However, perhaps this problem can be ameliorated by providing a static analysis tool that tells the programmer where the potential data races are, so that the programmer can insert the appropriate commands/annotations to specify an order of evaluation for the offending code.
There are many styles of presenting the meaning (semantics) of a programming language, and it's unclear which one is the best, or whether there are more styles or variations still yet be discovered that could make life easier for the working programming language designer. Perhaps the most natural style is called "big-step" semantics, which closely corresponds to a typical recursive interpreter. However, one problem with big-step semantics is that dealing with exceptions or other kinds of errors requires a large addition to the semantics: lots of extra rules that say how to propagate exceptions. In the context of an interpreter, this problem is often dealt with by writing the interpreter in "monadic" style, which enables the separation of the normal program logic from the error-handling logic, and condenses the error handling logic to just a few lines of code. The crazy idea/question then is whether monads can be adapted to big-step semantics, that is, adapting monads from their usual functional setting into a relational setting. Alternatively, instead of using relations to specify semantics, perhaps we should be using functions (i.e., simply writing interpreters).
According to Amer's very non-thorough survey of code-obfuscation literature, existing techniques are "best effort": i.e., they do bad things with code and hope that these things make code hard to understand.
Could we do probably-hard code obfuscation?
The basic idea is that between each pair of statements (or maybe at a coarser granularity) is a "lock". To determine if control flows from the first to the second statement, one needs to "unlock" the lock. This lock is carefully picked so that unlocking it is a known hard problem, say NP-Hard.
My first idea is to use pointer analysis. Horwitz's LOPLAS paper shows that precise flow-insensitive points-to analysis with multi-level pointers is NP-Hard. Could we structure the code so that the results of a points-to analysis is used as a hash function into a table of table of labels. If you do the pointer analysis precisely, the table lookup gets you the label of the next statement; if you do not do it precisely or do it incorrectly, it gives you the wrong label.
Aaron pointed out that obfuscation that is provably hard for a static analysis may not be provably hard for a dynamic analysis; specifically we could just run the program and see how the control flows. This will require some thought to determine if it is a fatal flaw.