Biblio

The semaphore mechanism is an important part of the embedded operating system. Therefore, it is very necessary to ensure its safety. Traditional software testing methods are difficult to ensure 100% coverage of the program. Therefore, it is necessary to adopt a formal verfication method which proves the correctness of the program theoretically. This paper proposes a proof framework based on the theorem proof tool Coq: modeling the semaphore mechanism, extracting important properties from the requirement documents, and finally verifying that the semaphore mechanism can meet these properties, which means the correctness of the semaphore mechanism is proved and also illustrates the feasibility of the verification framework proposed in this paper, which lays a foundation for the verification of other modules of operating systems.

Let Addk,N denote the Boolean function which takes as input k strings of N bits each, representing k numbers a(1),…,a(k) in \0,1,…,2N−1\, and outputs 1 if and only if a(1) + ⋯ + a(k) ≥ 2N. Let MAJt,n denote a monotone unweighted threshold gate, i.e., the Boolean function which takes as input a single string x ∈ \0,1\n and outputs 1 if and only if x1 + ⋯ + xn ≥ t. The function Addk,N may be viewed as a monotone function that performs addition, and MAJt,n may be viewed as a monotone gate that performs counting. We refer to circuits that are composed of MAJ gates as monotone majority circuits. The main result of this paper is an exponential lower bound on the size of bounded-depth monotone majority circuits that compute Addk,N. More precisely, we show that for any constant d ≥ 2, any depth-d monotone majority circuit that computes Addd,N must have size 2Ω(N1/d). As Addk,N can be computed by a single monotone weighted threshold gate (that uses exponentially large weights), our lower bound implies that constant-depth monotone majority circuits require exponential size to simulate monotone weighted threshold gates. This answers a question posed by Goldmann and Karpinski (STOC’93) and recently restated by Håstad (2010, 2014). We also show that our lower bound is essentially best possible, by constructing a depth-d, size 2O(N1/d) monotone majority circuit for Addd,N. As a corollary of our lower bound, we significantly strengthen a classical theorem in circuit complexity due to Ajtai and Gurevich (JACM’87). They exhibited a monotone function that is in AC0 but requires super-polynomial size for any constant-depth monotone circuit composed of unbounded fan-in AND and OR gates. We describe a monotone function that is in depth-3 AC0 but requires exponential size monotone circuits of any constant depth, even if the circuits are composed of MAJ gates.

In 2007, Shacham published a seminal paper on Return-Oriented Programming (ROP), the first systematic formulation of code reuse. The paper has been highly influential, profoundly shaping the way we still think about code reuse today: an attacker analyzes the "geometry" of victim binary code to locate gadgets and chains these to craft an exploit. This model has spurred much research, with a rapid progression of increasingly sophisticated code reuse attacks and defenses over time. After ten years, the common perception is that state-of-the-art code reuse defenses are effective in significantly raising the bar and making attacks exceedingly hard. In this paper, we challenge this perception and show that an attacker going beyond "geometry" (static analysis) and considering the "dynamics" (dynamic analysis) of a victim program can easily find function call gadgets even in the presence of state-of-the-art code-reuse defenses. To support our claims, we present Newton, a run-time gadget-discovery framework based on constraint-driven dynamic taint analysis. Newton can model a broad range of defenses by mapping their properties into simple, stackable, reusable constraints, and automatically generate gadgets that comply with these constraints. Using Newton, we systematically map and compare state-of-the-art defenses, demonstrating that even simple interactions with popular server programs are adequate for finding gadgets for all state-of-the-art code-reuse defenses. We conclude with an nginx case study, which shows that a Newton-enabled attacker can craft attacks which comply with the restrictions of advanced defenses, such as CPI and context-sensitive CFI.