Runtime Verification of Linux Kernel Security Module

Denis Efremov; Ilya Shchepetkov

Runtime Verification of Linux Kernel Security Module

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2001.01442 v1 pith:SFWXGMFB submitted 2020-01-06 cs.SE cs.OS

Denis Efremov , Ilya Shchepetkov This is my paper · ORCID

classification cs.SEcs.OS

keywords securitylinuxsystemcallkernelpolicyaccessesconformance

verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments

read the original abstract

The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It is installed on billions of devices all over the world, which process various sensitive, confidential or simply private data. It is crucial to establish and prove its security properties. This work-in-progress paper presents a method to verify the Linux kernel for conformance with an abstract security policy model written in the Event-B specification language. The method is based on system call tracing and aims at checking that the results of system call execution do not lead to accesses that violate security policy requirements. As a basis for it, we use an additional Event-B specification of the Linux system call interface that is formally proved to satisfy all the requirements of the security policy model. In order to perform the conformance checks we use it to reproduce intercepted system calls and verify accesses.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Machine Learning-Based Security Policy Analysis
cs.LG 2024-12 reject novelty 4.0 of 10

A graph-based ML pipeline reports 95% accuracy detecting synthetic SELinux policy violations, but post-hoc violation-class refinement and no real-policy evaluation weaken the central claim.

Pith tools