Security-Enhanced Linux (SELinux) is a module of Linux operating system (OS) kernel providing enhanced security via full control over all interactions of software. It is a widely deployed security solution across technology-intensive industries, getting increased recognition from finances and military. The SELinux policy rules, which describe the access permissions, are developed and maintained manually by security engineers. Policy development is therefore slow, expensive and error-prone. Recent development of static software analysis, symbolic execution, and corresponding tools (such as Klee) enables the possibility to gain insight on how programs interacts in an OS and which resources they use.
Detailed insight in this area on the POSIX API level would vastly improve and automate SELinux policy development, causing a leap in the development of practical security. The aim of this project is to modify, develop, combine, and optimize static analysis and symbolic execution algorithms and their implementations to enable SELinux-oriented analysis of program source code. The main goal is to develop a tool automatically generating all possible SELinux policy rules eventually needed by the application. Additionally, the developed tool will detect existing policy rules that are never used and execution paths violating existing policy.
|
Contents
|
We agreed there are basically three challenges:
Given an application, find all possible rules (including labels) eventually needed by the application.
This challenge can be probably solved by static analysis. In the case that static analysis will not produce satisfactory information about possible labels for each rule, we can use symbolic execution (forward or backward) to compute an incomplete set of relevant labels.
Detect policy rules that are never used (dead rules).
A policy rule can be never used for two reasons:
It should be fairly easy to detect dead rules of type (i). Dead rules of type (ii) can be easily detected by solving the the first challenge.
Find execution paths in the application violating the current policy.
We expect that an algorithm solving the first challenge can also provide execution paths for each generated rule. After filtering out the paths for current policy rules, we get paths violating policy.
To sum up, the crucial challenge is the first one. To make some step towards its solution, we would need relatively small (but not trivial) piece of code and the corresponding policy.
It is difficult to write a new policy for a program. Generating
some reasonable (not necessarily complete or bug-free) policy
automatically would be helpful. Currently,
the sepolgen
tool is used to generate basic policy for a binary. The process
is as follows: run sepolgen on a binary to generate a
policy, enable the policy, run the program, watch for policy
violations. When a violation occurs, add the missing rule to the
policy and repeat (enable the fixed policy, run, watch). Obviously,
the policy writer fails to use all program features/supported
configurations/code paths, because programs are complicated. The
policy is not complete and users need to file bugs when they suffer
from an unjust AVC denial. When the policy is used for a few months
in production (in Fedora) without a violation, it is considered to
be usable.
The sepolgen tool runs nm -D to list functions used by
the binary and generates policy from that. This means that rules for
syscalls which are allowed as a whole by their name and their
parameters do not matter (e.g. allowing process to chroot, or to
call setuid/setgid) are
discovered. Nevertheless, most of SELinux rules confine access to
resources such as files, sockets, pipes and network interfaces. For
example a binary is only allowed to open and read a single file (its
config file). With nm -D you only know that
the open
function is called, but to generate a policy, you need to know
which files the binary will open
(or chown/chmod/stat...),
which directories it wants to read from or write to — tracking
and understanding function parameters is necessary here.
We can use dynamic execution to track the code that generates paths
used for syscalls such
as open/chown/stat, and also
track opened file descriptors. File paths are often read from a
configuration file or other input (socket), so important part of
this work would be to enable the possibility to model the program
environment well, for example we should allow to supply a list of
various possible (=supported) configuration file contents when the
symbolically executed program need to read one.
It is helpful to discover rules which are "dead": present in a policy, but never used by the application. There will be many of them, because programs evolve a lot over time, rules are added to a policy to support new versions of the application and to deal with application bugs which are then fixed, but rules are never removed from policies because of the risk of breaking some corner case configuration.
To discover superfluous rules, we need to understand the policy as it is written by developers (we need a parser). They use M4 macros to generate some rules. The policy sources are expanded by M4 preprocessor, and resulting policy text is compiled to a binary representation, which is loaded by kernel. I have asked several people about a parser understanding the policy source, but it seems it doesn't exist. I have found a partial parser in sepolgen, but haven't checked what's missing.
It is helpful to find all code paths in a program that break a SELinux policy. If we can do the previous two tasks, we should get this one almost for free.
The referential SELinux policy is available via Subversion (see the policy/modules/services subdirectory). Fedora policy is heavily modified, and it can be obtained most easily from a Fedora system:
$ fedpkg clone selinux-policy --anonymous
$ cd selinux-policy
$ fedpkg prep
$ less serefpolicy-3.9.16/policy/modules/services/apache.{fc,if,te}
SELinux policy consists only of allow rules. When a program has a policy, it can only do what the policy allows to do.
User Guide to SELinux is worth reading. See also references section for SELinux in Fedora Security Guide.
First, we develop a prototype tool applicable on selected small programs written in C, and providing satisfactory results on a subset of SELinux policy rules. Then we extend and optimize the tool to support wider range of programs and SELinux policy rules. Finally, we plan to develop an open source tool capable of checking large systems (e.g., Red Hat Enterprise Linux).
Systemd seems to be the right test application: it consists of ~3 MB of well written low-level C code that uses several widely used libraries and interacts with many SELinux controlled parts of a system (files, file attributes, processes, sockets, DBus, cgroups). It compiles quickly. Its SELinux policy is sufficiently interesting, but without user options that introduce unnecessary complexity.
http://www.freedesktop.org/software/systemd/
The SELinux policy for systemd can be obtained from Fedora selinux-policy package:
$ fedpkg clone selinux-policy $ cd selinux-policy; fedpkg prep $ ls ./serefpolicy-3.10.0/policy/modules/system/systemd.* ./serefpolicy-3.10.0/policy/modules/system/systemd.fc ./serefpolicy-3.10.0/policy/modules/system/systemd.if ./serefpolicy-3.10.0/policy/modules/system/systemd.te
Environment model simulates the environment the program runs in: the environment variables, user id, group id, file descriptors, user database, terminal, filesystem, sysfs, devfs. It also contains testing implementation of system calls and some other functions. Environment model can simulate that the program is run as normal user, or as root user. It can simulate the run with certain config file or system setup.
Program LLVM bitcode is provided
by LLVM IR service. It contains
all the shared libraries statically linked, so all the program code is
available, except the code run via dlopen()
and exec()
calls. Systemd
has been selected as the testing program for development: it consists
of ~3 MB of well written low-level C code that uses several widely
used libraries and interacts with many SELinux controlled parts of a
system (files, file attributes, processes, sockets, DBus, cgroups). It
compiles quickly. Its SELinux policy is sufficiently interesting, but
without user options (booleans) that introduce unnecessary
complexity.
Kernel LLVM bitcode is provided by LLVM IR service as well.
Kernel analysis: kernel/security/selinux/hooks.c, kernel/include/linux/security.h. The list of SELinux permission types is located in in libselinux/include/selinux/av_permissions.h
SELinux policy analysis: generate a new policy, find unused rules of the existing policy, find code paths causing AVC denial within current policy.