scholarly journals Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-31
Author(s):  
Marco Campion ◽  
Mila Dalla Preda ◽  
Roberto Giacobazzi

Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision. Then, we introduce a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis. Our framework is general enough to be instantiated to most known metrics for abstract domains.

Author(s):  
Marcos Lordello Chaim ◽  
Daniel Soares Santos ◽  
Daniela Soares Cruzes

Buffer overflow (BO) is a well-known and widely exploited security vulnerability. Despite the extensive body of research, BO is still a threat menacing security-critical applications. The authors present a comprehensive systematic review on techniques intended to detecting BO vulnerabilities before releasing a software to production. They found that most of the studies addresses several vulnerabilities or memory errors, being not specific to BO detection. The authors organized them in seven categories: program analysis, testing, computational intelligence, symbolic execution, models, and code inspection. Program analysis, testing and code inspection techniques are available for use by the practitioner. However, program analysis adoption is hindered by the high number of false alarms; testing is broadly used but in ad hoc manner; and code inspection can be used in practice provided it is added as a task of the software development process. New techniques combining object code analysis with techniques from different categories seem a promising research avenue towards practical BO detection.


1981 ◽  
Vol 10 (131) ◽  
Author(s):  
Flemming Nielson

<p>Abstract Interpretation (P. Cousot, R. Cousot and others) is a method for program analysis that is able to describe many data flow analyses. We investigate and weaken the assumptions made in abstract interpretation and express abstract interpretation within Denotational Semantics. As an example we specify constant propagation.</p><p>Some authors have used abstract interpretation to formulate ''available expressions'' (a so-called ''history-sensitive'' data flow analysis). Our development of ''available expressions'' is better justified, semantically.</p><p>In traditional data flow analysis and abstract interpretation it is generally assumed that the ''Meet Over all Paths'' solution is wanted. We prove that the solution specified by our approach is the ''Meet Over all Paths'' solution to a certain system of equations obtained from the program.</p><p>To indicate the usefulness of our approach we show how to validate a class of program transformations, including ''constant folding''.</p><p>Throughout this paper we use a toy language consisting of declarations, expressions and commands (involving conditional and iteration). Excluded are procedures and jumps.</p>


2014 ◽  
Vol 26 (4) ◽  
pp. 658-701 ◽  
Author(s):  
ROBERTO GIACOBAZZI ◽  
ISABELLA MASTROENI

Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.


2021 ◽  
Vol 16 (92) ◽  
pp. 103-122
Author(s):  
Victor V. Erokhin ◽  
◽  
Larisa S. Pritchina ◽  

The article discusses the problem of detecting and filtering shellcode – malicious executable code that contributes to the emergence of vulnerabilities in the operation of software applications with memory. The main such vulnerabilities are stack overflow, database overflow, and some other operating system service procedures. Currently, there are several dozen shellcode detection systems using both static and dynamic program analysis. Monitoring of existing systems has shown that methods with low computational complexity are characterized by a large percentage of false positives. Moreover, methods with a low percentage of false alarms are characterized by increased computational complexity. However, none of the currently existing solutions is able to detect all existing classes of shellcodes. This makes existing shellcode detection systems weakly applicable to real network links. Thus, the article discusses the problem of analyzing shellcode detection systems that provide complete detection of existing classes of shellcodes and are characterized by acceptable computational complexity and a small number of false alarms. This article introduces shellcode classifications and a comprehensive method of detecting them based on code emulation. This approach expands the detection range of shellcode classes that can be detected by concurrently evaluating several heuristics that correspond to low-level CPU operations during execution of various shellcode classes. The presented method allows efficient detection of simple and metamorphic shellcode. This is achieved regardless of the use of self-modifying code or dynamic code generation on which existing emulation-based polymorphic shellcode detectors are based.


Author(s):  
I.F. Lozovskiy

The use of broadband souding signals in radars, which has become real in recent years, leads to a significant reduction in the size of resolution elements in range and, accordingly, in the size of the window in which the training sample is formed, which is used to adapt the detection threshold in signal detection algorithms with a constant level of false alarms. In existing radars, such a window would lead to huge losses. The purpose of the work was to study the most rational options for constructing detectors with a constant level of false alarms in radars with broadband sounding signals. The problem was solved for the Rayleigh distribution of the envelope of the noise and a number of non-Rayleigh laws — Weibull and the lognormal, the appearance of which is associated with a decrease in the number of reflecting elements in the resolution volume. For Rayleigh interference, an algorithm is proposed with a multi-channel in range incoherent signal amplitude storage and normalization to the larger of the two estimates of the interference power in the range segments. The detection threshold in it adapts not only to the interference power, but also to the magnitude of the «power jump» in range, which allows reducing the number of false alarms during sudden changes in the interference power – the increase in the probability of false alarms did not exceed one order of magnitude. In this algorithm, there is a certain increase in losses associated with incoherent accumulation of signals reflected from target elements, and losses can be reduced by certain increasing the size of the distance segments that make up the window. Algorithms for detecting broadband signals against interference with non-Rayleigh laws of distribution of the envelope – Weibull and lognormal, based on the addition of the algorithm for detecting signals by non-linear transformation of sample counts into counts with a Rayleigh distribution, are studied. The structure of the detection algorithm remains unchanged in practice. The options for detectors of narrowband and broadband signals are considered. It was found that, in contrast to algorithms designed for the Rayleigh distribution, these algorithms provide a stable level of false alarms regardless of the values of the parameters of non-Rayleigh interference. To reduce losses due to interference with the distribution of amplitudes according to the Rayleigh law, detectors consisting of two channels are used, in which one of the channels is tuned for interference with the Rayleigh distribution, and the other for lognormal or Weibull interference. Channels are switched according to special distribution type recognition algorithms. In such detectors, however, there is a certain increase in the probability of false alarms in a rather narrow range of non-Rayleigh interference parameters, where their distribution approaches the Rayleigh distribution. It is shown that when using broadband signals, there is a noticeable decrease in detection losses in non-Rayleigh noise due to lower detection thresholds for in range signal amplitudes incoherent storage.


1980 ◽  
Vol 33 (3) ◽  
pp. 475-481
Author(s):  
P. Bertolazzi ◽  
M. Lucertini

The major purpose of an air traffic control system is to ensure the separation of two or more aircraft flying in the same airspace, with an efficiency that can be expressed in terms of capacity and cost. As air traffic grows in numbers it becomes necessary to reduce the workload of the controllers by relieving them of many monitoring tasks, and eventually some decision-making tasks, through computerized automation. In this context many developments tend to build up an efficient conflict-alert subsystem.The problem of conflict-alert in the air needs strategic tools, to make collision unlikely or even impossible, and tactical tools to detect impending collisions. The latter detect potentially hazardous aircraft encounters and alert the controller in time to warn the pilots (if necessary) and should obviously provide this capability with a minimal number of false alarms and no increase in workload.


2011 ◽  
Vol 29 ◽  
pp. 61-67 ◽  
Author(s):  
H.-J. Bao ◽  
L.-N. Zhao ◽  
Y. He ◽  
Z.-J. Li ◽  
F. Wetterhall ◽  
...  

Abstract. The incorporation of numerical weather predictions (NWP) into a flood forecasting system can increase forecast lead times from a few hours to a few days. A single NWP forecast from a single forecast centre, however, is insufficient as it involves considerable non-predictable uncertainties and lead to a high number of false alarms. The availability of global ensemble numerical weather prediction systems through the THORPEX Interactive Grand Global Ensemble' (TIGGE) offers a new opportunity for flood forecast. The Grid-Xinanjiang distributed hydrological model, which is based on the Xinanjiang model theory and the topographical information of each grid cell extracted from the Digital Elevation Model (DEM), is coupled with ensemble weather predictions based on the TIGGE database (CMC, CMA, ECWMF, UKMO, NCEP) for flood forecast. This paper presents a case study using the coupled flood forecasting model on the Xixian catchment (a drainage area of 8826 km2) located in Henan province, China. A probabilistic discharge is provided as the end product of flood forecast. Results show that the association of the Grid-Xinanjiang model and the TIGGE database gives a promising tool for an early warning of flood events several days ahead.


Author(s):  
С.Б. Егоров ◽  
Р.И. Горбачев

«Выбросовая» вероятностная модель работы обнаружителя в режиме ожидания сигнала, предложенная авторами в [1], использована для оценки влияния селекции выбросов по длительности на вероятность ложной тревоги. Флюктуационные выбросы помехового индикаторного процесса, превысившие пороги селекции по уровню и длительности, трактуются как редкие события на интервале ожидания сигнала, подчиняющиеся вероятностному закону Пуассона. При условии, что средний период следования ложных выбросов превышает интервал корреляции индикаторного процесса, получено соотношение между средним числом выбросов любой длительности и средним числом выбросов, превысивших пороговую длительность. На основании известных числовых и вероятностных характеристик выбросов нормального стационарного случайного процесса получен уравнения, связывающие относительные пороги селекции по уровню и длительности с вероятностью ложной тревоги на интервале ожидания сигнала. Предложена методика определения порога селекции по длительности для снижения порога селекции по уровню до заданной величины. «Emissional» probability model of the detector in stand-by mode proposed by the authors in [1], is intended for estimation of false alarm rate dependence from the value of time-selection threshold. Fluctuation emissions of the noise indicator process are interpreted as rare events correspond to Poisson distribution. Assuming that average rate of false alarms exceeds the correlation interval of indicator process, obtained equation between average number of false alarms of any duration and average number of false alarms exceed the time threshold. Based on known numerical and statistical characteristics of emissions of normal stationary random process obtained equations, relating time and level thresholds with false alarm probability on stand-by mode time interval. Also suggested a method of determining time threshold intended to reduce level threshold.


Sign in / Sign up

Export Citation Format

Share Document