The path examiner, 2nd edition, is a GCC plugin that works on a function to verify if there are paths in the CFG from the top of the function to special function calls labelled kayrebt_FlowNodeMarker without passing by LSM hooks (functions starting with security_. The analysis is run during the compilation, on the CFG in Static Single Assignment form, after most optimizations are performed.
The sources of the path examiner are available on the Inria forge.
Here is the direct link to the git repository (anonymous read-only access):
The requirements to build the path examiner are:
- g++ version 4.8 exactly,
- the Yices SMT solver.
The path examiner is packaged with the autotools. If you download
a tarball, the build process is as simple as:
./configure make make install
To run the path examiner, you need a compilable source file. In this source file, you have to mark manually the target statements. You do this by declaring a function void kayrebt_FlowNodeMarker(void); and placing function calls to this function in the function you want to analyze. The analysis will return the number of execution paths from the root of the function to each marked place which have been proven to be impossible to take at runtime, and the number of execution paths which may be possible.
Our raw results can be examined in the repository https://scm.gforge.inria.fr/anonscm/git/kayrebt/Linux.git in the branch results, in the directory patches.
Proposal to patch the Linux kernel v4.3 to add missing hooks
After running the analysis against the kernel v4.3, we came to the conclusion that LSM was perfectly suitable for information flow control after some modifications. The following patches describe them. They are to be applied against the commit tagged v4.3. You can also pull the branch hooks-for-ifc in our clone of the Linux repository: https://scm.gforge.inria.fr/anonscm/git/kayrebt/Linux.git.
- [PATCH 1/4] Add LSM hooks in vmsplice, splice, and tee
- [PATCH 2/4] Add LSM hooks for munmap and shmdt
- [PATCH 3/4] Add LSM hooks for mq_timedsend and mq_timedreceive
- [PATCH 4/4] Move LSM hooks in recvmmsg and sendmmsg
The source code of the path examiner is documented with Doxygen and the documentation is available here.