[Draft] Goblint enhacements for Linux kernel analysis

[jprotopopov-ut]

This issue will be used as a draft to document necessary enhancements in Goblint to extend the scope and precision Linux kernel analysis. Certain issues might be opened towards the upstream Goblint repository later on

[jprotopopov-ut]

Kernel-specific
Linux kernel relies on non-standard features to publish module API. For instance, section and alias attributes are used to expose certain elements of module API to the rest of the kernel. In actual execution, the kernel handles it via accessing respective sections of ELF image. During static analysis, reliable access to these API is problematic.

Currently, the issue is resolved by applying a minimal patch that trivially exposes respective API elements by removing static storage qualifiers. This needs to be addressed more generally, either by enhancing Goblint to expose API elements marked by respective attributes, or by introducing a mechanism for ad-hoc user-defined exposure of certain API elements for analysis

[jprotopopov-ut]

Precision enhancements
Precision loss in analysis of space-separated accesses produces false positives. lp driver seems to provide a good example of this, as it exhibits concurrent accesses separated by array indexes with per-index locks.
Overall, I believe, https://dl.acm.org/doi/pdf/10.1145/3732933 provides a good overview of concurrency patterns that are not well-handled yet, but might be beneficial in both userspace and kernel analysis

[jprotopopov-ut]

Precision enhancements 2
Goblint seems to exhibit certain arbitrary precision loss depending on thread creation order. For instance, the following example generates different race analysis results depending on where the "driver" thread is created. This is mitigated by more deliberate order of thread initialization in the generated harnesses, but this mitigation is arbitrary.

./goblint --conf conf/examples/very-precise.json ~/1.c

// 1.c
#include <pthread.h>

struct ttyprintk_port {
       pthread_mutex_t lock;
};

static struct tty_driver *ttyprintk_driver;
static struct ttyprintk_port tpk_port;
struct ttyprintk_port *(*open)();
static int X = 0;

static struct ttyprintk_port *tpk_open() {
  return &tpk_port;
}

static void *process_tty_client2(void *arg) {
  struct ttyprintk_port *tpkp = open();
  for (int i = 0; i < 1; i++) {
    pthread_mutex_lock(&tpkp->lock);
    X = 1;
    pthread_mutex_unlock(&tpkp->lock);
  }
  return NULL;
}

static void *process_tty_driver(void *arg) {
  open = tpk_open;
  return NULL;
}

int main() {
  pthread_t process_thread_tty_client1;
  pthread_t process_thread_tty_client2;
  pthread_t process_thread_tty_driver;
  
       pthread_mutex_init(&tpk_port.lock, NULL);

  // pthread_create(&process_thread_tty_driver, NULL, process_tty_driver, NULL);
  pthread_create(&process_thread_tty_client1, NULL, process_tty_client2, NULL);
  pthread_create(&process_thread_tty_client2, NULL, process_tty_client2, NULL);
  pthread_create(&process_thread_tty_driver, NULL, process_tty_driver, NULL);
  
  pthread_join(process_thread_tty_driver, NULL);
  pthread_join(process_thread_tty_client1, NULL);
  pthread_join(process_thread_tty_client2, NULL);
  
  return 0;
}

[jprotopopov-ut]

Kernel-specific 2
Goblint does not support certain built-ins that are of widespread use in kernel networking subsystem, which precludes analysis of respective modules. In particular, htons type builtins are ubiquitous in include/net/inet_ecn.h

[jprotopopov-ut]

Precision enhancements 3
Goblint has been observed to exhibit precision loss in race analysis depending on escaped object storage. In particular, objects allocated on stack produce more precise analysis results than those allocated on heap (even if heap allocation is one-off deliberate memory leak). Speculatively, the issue seems to be due to drop of precision of escape analysis, however this has not been investigated. The issue was revealed in harness encoding generation, and mitigated by implementing some particular encoding. Nevertheless, the mitigation is arbitrary and the issue might have broader impact on precision of kernel module analysis.

// Example requires more deliberate setup. To be done

[jprotopopov-ut]

Performance and resource consumption
In certain cases (e.g. driver/char/random.c), Goblint exhibits high memory usage and unreasonable run times even for simple environment models. While this is natural and expected, extent of the issue and opportunities for improvement have not been investigated