scholarly journals Procedure-modular verification of control flow safety properties

2010 ◽  
Author(s):  
Siavash Soleimanifard ◽  
Dilian Gurov ◽  
Marieke Huisman
Keyword(s):  
Control Flow ◽  
Safety Properties ◽  
Modular Verification

scholarly journals Higher order symbolic execution for contract verification and refutation

2016 ◽  
Vol 27 ◽  
Author(s):  
PHÚC C. NGUYÊN ◽  
SAM TOBIN-HOCHSTADT ◽  
DAVID VAN HORN
Keyword(s):  
Symbolic Execution ◽  
Type Systems ◽  
Higher Order ◽  
Control Flow ◽  
Test Case ◽  
Modular Verification ◽  
Automated Test Case Generation ◽  
Behavioral Contracts ◽  
Virtuous Cycle ◽  
And Control

AbstractWe present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. To validate our approach, we use it to develop and evaluate a system for verifying and refuting behavioral software contracts of components in a functional language, which we call soft contract verification. In doing so, we discover a mutually beneficial relation between behavioral contracts and higher-order symbolic execution. Contracts aid symbolic execution by providing a rich language of specifications serving as a basis of symbolic higher-order values; the theory of blame enables modular verification and leads to the theorem that verified components can't be blamed; and the run-time monitoring of contracts enables soft verification whereby verified and unverified components can safely interact. Conversely, symbolic execution aids contracts by providing compile-time verification and automated test case generation from counter-examples to verification. This relation between symbolic exuection and contracts engenders a virtuous cycle encouraging the gradual use of contracts.Our approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of off-the-shelf solvers to decide problems without heavy encodings. Counterexample search is sound and relatively complete with respect to a first-order solver for base type values and counter-examples are reported as concrete values, including functions. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. The approach is competitive with a range of existing tools—including type systems, flow analyzers, and model checkers—on their own benchmarks. We have built a prototype to analyze programs written in Racket and report on its effectiveness in verifying and refuting contracts.

scholarly journals Robustly Safe Compilation, an Efficient Form of Secure Compilation

2021 ◽  
Vol 43 (1) ◽  
pp. 1-41
Author(s):  
Marco Patrignani ◽  
Deepak Garg
Keyword(s):  
Control Flow ◽  
Target Level ◽  
Safety Properties ◽  
Source Program ◽  
Protection Mechanisms ◽  
Efficient Code ◽  
Proof Techniques ◽  
Compiled Code ◽  
Target Languages ◽  
The Cost

Security-preserving compilers generate compiled code that withstands target-level attacks such as alteration of control flow, data leaks, or memory corruption. Many existing security-preserving compilers are proven to be fully abstract, meaning that they reflect and preserve observational equivalence. Fully abstract compilation is strong and useful but, in certain cases, comes at the cost of requiring expensive runtime constructs in compiled code. These constructs may have no relevance for security, but are needed to accommodate differences between the source and target languages that fully abstract compilation necessarily needs. As an alternative to fully abstract compilation, this article explores a different criterion for secure compilation called robustly safe compilation or RSC . Briefly, this criterion means that the compiled code preserves relevant safety properties of the source program against all adversarial contexts interacting with the compiled program. We show that RSC can be proved more easily than fully abstract compilation and also often results in more efficient code. We also present two different proof techniques for establishing that a compiler attains RSC and, to illustrate them, develop three illustrative robustly safe compilers that rely on different target-level protection mechanisms. We then proceed to turn one of our compilers into a fully abstract one and through this example argue that proving RSC can be simpler than proving full abstraction. To better explain and clarify notions, this article uses syntax highlighting in a way that colourblind and black-8-white readers can benefit from Reference [58]. For a better experience, please print or view this article in colour . 1

Lightweight Fault Localization using Weighted Dynamic Control Flow Subgraph

2020 ◽  
Vol 16 (2) ◽  
pp. 214
Author(s):  
Wang Yong ◽  
Liu SanMing ◽  
Li Jun ◽  
Cheng Xiangyu ◽  
Zhou Wan
Keyword(s):  
Dynamic Control ◽  
Fault Localization ◽  
Control Flow

Numerical Investigation of Passive Flow Control Using Wavy Blades in a Highly-Loaded Compressor Cascade

2018 ◽  
Author(s):  
Bo Wang ◽  
Yanhui Wu ◽  
Kai Liu
Keyword(s):  
Numerical Investigation ◽  
Flow Structure ◽  
Cross Flow ◽  
Leading Edge ◽  
Control Flow ◽  
Streamwise Vortices ◽  
Compressor Cascade ◽  
Control Effect ◽  
Suction Surface ◽  
Highly Loaded

Driven by the need to control flow separations in highly loaded compressors, a numerical investigation is carried out to study the control effect of wavy blades in a linear compressor cascade. Two types of wavy blades are studied with wavy blade-A having a sinusoidal leading edge, while wavy blade-B having pitchwise sinusoidal variation in the stacking line. The influence of wavy blades on the cascade performance is evaluated at incidences from −1° to +9°. For the wavy blade-A with suitable waviness parameters, the cascade diffusion capacity is enhanced accompanied by the loss reduction under high incidence conditions where 2D separation is the dominant flow structure on the suction surface of the unmodified blade. For well-designed wavy blade-B, the improvement of cascade performance is achieved under low incidence conditions where 3D corner separation is the dominant flow structure on the suction surface of the baseline blade. The influence of waviness parameters on the control effect is also discussed by comparing the performance of cascades with different wavy blade configurations. Detailed analysis of the predicted flow field shows that both the wavy blade-A and wavy blade-B have capacity to control flow separation in the cascade but their control mechanism are different. For wavy blade-A, the wavy leading edge results in the formation of counter-rotating streamwise vortices downstream of trough. These streamwise vortices can not only enhance momentum exchange between the outer flow and blade boundary layer, but also act as the suction surface fence to hamper the upwash of low momentum fluid driven by cross flow. For wavy blade-B, the wavy surface on the blade leads to a reduction of the cross flow upwash by influencing the spanwise distribution of the suction surface static pressure and guiding the upwash flow.

Sign in / Sign up

Export Citation Format

Share Document