System call whitelisting is a powerful sandboxing approach that can significantly reduce the capabilities of an attacker if an application is compromised. Given a \emph{policy} that specifies which system calls can be invoked with what arguments, a sandboxing framework terminates any execution that violates the policy.
While this mechanism greatly reduces the attack surface of a system, manually constructing these policies is time-consuming and error-prone. As a result, many applications —including those that take untrusted user input— opt not to use a system call sandbox.

Motivated by this problem, we propose a technique for automatically constructing system call whitelisting policies for a given application and policy DSL. Our method combines static code analysis and program synthesis to construct \emph{sound and precise policies} that never erroneously terminate the application, while restricting the program's system call usage as much as possible.
We have implemented our approach in a tool called \textsc{Abhaya}\xspace and experimentally evaluate it 493 Linux and OpenBSD applications by automatically synthesizing {Seccomp-bpf}\xspace and \text{Pledge}\xspace policies. Our experimental results indicate that \textsc{Abhaya}\xspace can efficiently generate useful and precise sandboxes for real-world applications.