Detecting Code Security Breaches by Means of Dataflow Analysis Sergei Borzykh Alexey Markov, Valentin Tsirlov Alexander Barabanov Development Department Information Security Department Testing Department NPO Echelon, JSC Bauman Moscow State Technical NPO Echelon, JSC University Moscow, Russia Moscow, Russia Moscow, Russia mail@npo-echelon.com a.markov@bmstu.ru, v.tsirlov@bmstu.ru ab@cnpo.ru Abstract—We discuss static and dynamic methods of the code automation of the tests for the program defects based on their analysis. A new approach to the static analysis method based on design features. When developing software for special-purpose command flow graphs is presented. Practical cases and informational systems, these methods are used to search for implementations of this dataflow approach are given. random code defects, and hidden software functionality (backdoors) [14, 15]. Keywords— information security; software security; static analysis; heuristic analysis; vulnerabilities; defects; production Dynamic software analysis is a method of analysis that models; data-flow analysis stipulates program running on real or virtual processor [16]. Functional testing is most in demand during the study of the programs by black box method, when there is access to only I. INTRODUCTION external software interfaces without account of their structure, back-end interfaces or status. The approach is used to study IT-based solutions are currently used everywhere, and accuracy and stability of the software operation within the significant problems are represented by both internal software framework of the key jobs of the test engineers, however, the errors of the information systems, and malicious source code method is not always effective for searching of errors related to implemented in the information system software. The combinations of rarely used input data, and for identifying consequences of both problems lead to violation of access, intentional backdoors there. Static analysis of the software integrity and confidentiality of the processed information, source texts is closely related to development of compilation which can result in financial and reputational losses of the systems, and many approaches of static analysis use elements business. This is a reason of growing financial losses over the of the compiler theory, namely, the code view models [17, 18]. last few years. High quality and failure-free operation of the source code is a burning issue of the software industry. Ever III. SIGNATURE ANALYSIS AS THE MAIN METHOD growing complexity of the software complexes, their use in the The approach that is called signature analysis implies the management and control systems of the government and the search for software defects in the software code by comparing industrial production require continuous upgrading of the code fragments with the samples from the database of templates software testing and control methods [1-11]. (signatures) of the security defects. Depending on the method II. STATIC AND DYNAMIC METHODS OF THE CODE for correlating fragments of the code to the template, and the ANALYSIS intermediate representation in use, there may be algorithms of searching for a substring in the string, and query language for Upon the whole, the testing methods used in the audit of the structured information (for instance, XQuery for XML), or software systems security may be divided into two groups: specially designed methods of correlation, but in each case each static methods (structural testing) and dynamic methods of the signatures represents the decision procedure, which (functional testing). Static methods of the code analysis, which employs various presence bits of potentially harmful structure. do not require running of the analysed code for its operation, [18] provides examples of the rules for generating error allow for full or partial automation [12, 13]. Such methods are signatures, which correspond to the CWE standard. We can see most frequently used in case of full access to the software here that the signature methods are not limited to the types of system and its source texts, which is called “a white-box defects and are preferable, when dealing with the backdoors. technique”. It employs source and loading modules of the program and its component. The benefit of the static code Improvement of the operational qualities of the static code analysis is that it does not require multiple program runs under analysis is mainly related to minimizing the number of “false various operational conditions (condition of the environment positives” while preserving maximum fullness of the list of the and input data) and possibility to achieve a greater degree of types of potentially harmful structures [19]. Therefore, the 15 instruments describing signatures of the code defects shall There is a mechanism for dataflow analysis called “taint ensure maximum flexibility in defining a defect with account of propagation”, which allows for identifying the defect, but also diversity in the syntax of the programming language under shows the data propagation path, starting from the entry point study. (user input), through the program and to the function vulnerability [29]. An interesting instance of such mechanism The field for designing means of static analysis is now of dataflow analysis is “constant propagation” - search for actively developing: new directions of analysis do not force out authentication data (login, password, IP-address) directly in the the reputable approaches, on the contrary, they complement software source code. Let us review a code fragment: them by integrating the advantages of the predecessors. For instance, such approach as dataflow analysis may compensate String login = "Some Constant"; for the drawbacks of the template-based code defect search, Such code fragment can be sought using signature analysis which does not allow for high quality of identification of SQL- (search as per templates). It only requires representation rule: , Path-, XSS-injections, and other types of code injections, however, it will require large RAM and computing resources of VARIABLE (“login” OR “password”) the processor [20, 21, 22]. OPERATOR (“=”) CONSTANT(*); An interesting manifestation of symbiosis of the analysis However, these code fragments can show that such code methods is when potentially harmful structures, which have was written for debugging and remained in the final software been initially identified by the customary signature method is version by accident, or was added intentionally, provided there supported by the automated method using highly-specialized, was assurance that the code would not be inspected. If a costly, but efficient procedures [23-25]. malicious developer wants to hide the imbedded defect from the person, who inspects the code, but also from the means of static IV. DATAFLOW ANALYSIS analysis, the code may be written, for instance, this way: The dataflow analysis can be described as a process of String label = "somewhere".substring(0,4); gathering information about the use, defining and dependency String summ = of data in the analysed program [26, 27]. The dataflow analysis LogConstant.class().getClassName().toLowerCase() uses command flow graph generated based on the code tree. ; This graph represents all possible paths for running this String upd_time = summ.substring(3, program: the nodes stand for ‘linear’, consecutive fragments of summ.lenght()-3); the code without any transitions, and the edges stand for Char ascii_conv = 95; String login = label + ascii_conv + upd_time; potential transfer of control between these fragments. If we break down parts of code fragment into various Syntactic analysis allows for identifying control structures, modules and files of source texts, it will be next to impossible such as procedure, function or method calls, which, in their to identify the defect using manual analysis, as well as many turn, allow building call graphs, control flow graphs, and known automated methods. identifying assignation and the others that allow building dataflow graphs [17, 18, 28]. Control and dataflow graphs are The “constant propagation” mechanism of the dataflow used for analysis of the local program blocks (mainly, the analysis may define the values of the variables, their content of the functions, procedures and methods - local concatenation and transfer into other variables, and final values analysis). Control flow graphs allow analysing program of the variables. As a result, the defect may be identified and, behaviour on a more general level (on the level of the file, consequently, unauthorized access to the functional capabilities module or the entire program - global analysis). of the software may be prevented. The dataflow analysis can be used for proper detection of V. OPERATING PRINCIPLES AND APPLICATION OF THE certain types of defects (as a rule, in operation) with a minimum DATAFLOW ANALYSIS number of false positives: SQL-, command-, XSS-injections, other types of code injections and setting directly in the code of Previous sections show the importance of static analysis and the authentication data. It should be noted that despite the general issues. Following sections describe the main approach differences in these defects, most of them implement the for dataflow analysis implementation and results of its following defect use pattern. implementation in static analyzer AppChecker developed by NPO Echelon. Let us introduce a set of definitions for a future 1. Data is received from the user (consequently, shorter description of the principles and algorithms of this untrusted data). method operation: 2. Data propagates through the program depending on the • Point — a node in the control flow graph; conditions and cycles. • Touch points (TP) (sink or critical points) — nodes in 3. Data is transformed, or filtered, or remains unchanged. the control flow graph, which are used for calling important 4. Finally, untrusted data gets access to the vulnerable functionality (in the context of the identified defect); function (buffer management, SQL query running • Entry point - nodes in the control flow graph, where etc.). new data is received from interfaces outside the analysed code; 16 • Untrusted data - data received from interfaces outside 3. If untrusted data were transmitted at the following the analysed code and trusted zone (allied agents, users); point of the critical control flow, proceed to clause 4. Otherwise, complete analysis of the current critical • Critical flow - flow from the entry point to the touch control flow. point. 4. If the current point is the endpoint, proceed to clause Let us define the general procedure for the search for 5. Otherwise, proceed to clause 2 with a new point and undocumented features using dataflow analysis: new input data. Continue, until analysis of all points in 1. Prepare source texts and configurations of the analysed the critical control flow is complete. software. 5. If the current point is the endpoint, and untrusted data 2. Use of the static analysis tools (that implement were transmitted to the potentially vulnerable function dataflow analysis) to sourced texts and configurations from the first point, enter the critical control flow on prepared in step 1. the positive triggering list. Otherwise, finalize analysis of the current critical control flow. 3. Processing of the results of analysis: The list obtained at the entry to the second stage of analysis • Selecting suspicious dataflow paths, is transferred to the entry of the report generator, which control • Analysing entry points and points of untrusted data interface is also present within the graphical user interface; after propagation, that the report generator based on the transferred list and database of the defect types draws up a report on the performed • Filtering false positives. static analysis. 4. Drawing up the final report. VI. LOCAL ANALYSIS Dataflow analysis is divided into two stages. The first stage The following description refers to dataflow of analysis requires engineering of critical control and implementation in static analyzer AppChecker developed by dataflows in the analysed software. Below is the sequence of NPO Echelon. The local analysis is normally performed for a the algorithm actions. certain block of the code (which coincides with the visibility 1. Search for the entry points of the untrusted data in the scope depending on the programming language). The local analyzed software (template-based search). This step analysis assumes obtaining information about the conditions of requires a base of entry points templates formed by the program in all points of the program, i.e.: inspections of standard libraries and popular • On creating data; frameworks. • On saving data; 2. Search for the points that contain potentially vulnerable functions (template-based search as well). • On destruction of data. 3. For each entry point of the untrusted data, add The diagram of the local analysis algorithm can be seen in function, method and procedure calls that are Figure 1. happening in this point to the control flow tree. You can optionally store, for instance, data on the value 4. Repeat clause 3 until you reach one of the final points constancy (for the “constant propagation” tool), data assurance specified in clause 2, or until you reach a point that flag (for “taint propagation”), and information about the does not transition into other functions, procedures or condition of the variable. methods. Information can be obtained from the local block in two 5. Once control flow trees are built, identify flows that opposite ways listed below: have reached potentially vulnerable functions. 1. From bottom to top: from the point susceptible to the Consider these flows critical. defect make assumptions about the properties of the At the second stage, analyse critical control flows, their data transmitted into it, go up the code to the point of separate points (functions, procedures and methods) and entry in the local area (function, procedure or method). identify the fact of untrusted data propagation from the entry The approach requires consideration of all options of point to the potentially vulnerable function. Below is the the program run (for each branch and iteration of the sequence of the algorithm actions: cycles), which leads to “combinatorial explosion” of the information quantity, which shall be stored during 1. Obtain entry point (function, procedure or method), analysis. engineer all dataflows that affect the data received from untrusted source. 2. From top to bottom — from the point of entry of untrusted data into the program, down along the code, 2. If untrusted data after interaction with other dataflows with available information about all of the above has not changed its status, proceed to clause 3. points of the program. This approach allows making Otherwise, complete analysis of the current critical assumptions about running separate branches of the control flow. program and engineer sequential analysis. The 17 drawback of this approach is difficulty in obtaining the path from the entry point to the exit point, because the only known fact is that the path exists. Fig. 2. Diagram of the Global Analysis Algorithm. VIII. MATHEMATICAL DESCRIPTION OF THE DATAFLOW ANALYSIS The ideal solution of the dataflow analysis task from the theoretical point of view consists in the search for all possible paths. Let us introduce certain symbols: B — data block for analysis, which consists from elementary subblocks B1, …, Bn. It is a known fact, that the dataflow values before the statement and after it are limited by the semantics of the instruction. The correlation between the dataflow values before and after the assignment statement is characterized by the transfer function. fi shall stand for a transfer function of block Bi, which characterizes transformation of data in this block. The values of the dataflow before and after subblock Bi shall be represented as IN[Bi] (OUT[Bi] accordingly). Fig. 1. Diagram of the Local Analysis Algorithm. Suppose P is a possible execution path in the flow graph: VII. GLOBAL ANALYSIS P= Input → B1 → … → Bk. Information that is available within one function (procedure, method), as a rule, is insufficient for high quality In this case, the transfer function fP for path P will be search for the defects, because many defects propagate represented by a composition of the transfer functions fk−1•…•f1. throughout the project, or, at least one file. Global analysis is However, it should be noted that fk is not a part of the used to link data received from different functions. The global composition, which shows that the path reached the start of analysis engages call graphs. To ensure operation of this subblock Bk, but not its end. Let us consider that any flow graph analysis it is sufficient to obtain certain confirmation or consists of two empty subblocks - input block, which is a start assumption about the properties of input and output data of point of the graph, and output block, which is passed by all exits separate functions in the call graph. It is important to obtain from the graph. The transfer functions of input and output such data in the context of the functions, which are outside of blocks are represented by constant values. the path from the point of the data entry to the point susceptible to the defects, and which analysis is necessary because the call Thus, taking into account the foregoing, the ideal solution is of such functions may change the arguments or return values, the array: which properties may depend on the properties of the input data (for instance, the substring get function, which accepts data 𝐼𝐷𝐸𝐴𝐿(𝐵) = ⋃𝑃 𝑓𝑃 (𝑣𝑖𝑛𝑝𝑢𝑡 ), input by the user returns taint data, although formally it is not where 𝑣𝑖𝑛𝑝𝑢𝑡 is the result of the constant transfer function, included in the call graph). which is represented by the starting input node. The diagram of the global analysis algorithm can be seen in It may seem that the task of the search for the ideal solution Figure 2. is reduced to analysis of the transfer functions fP for all paths P in the flow graph. However, it was noted by Ullmann [17, page 724], the task of the search for the ideal solution is generally unsolvable. If block B has branches, cycles and recursions, array IDEAL[B] maybe unlimited. The assistance comes from the solution of path-based gathering [17, page 757], which is similar to the path search algorithm in the graph, so called ‘breadth first search’. This algorithm allows achieving such 18 final number of P, that an array of all fP covers all unique 1. Potential SQL-injection is identified in Dolibarr transformations of fB. project, in htdocs/admin/menus/edit.php file: Let us write down an iterative solution to the generalized B284 = «$sql = "SELECT m.rowid, m.mainmenu, m.level, task for the dataflow. There are two versions of such m.langs FROM ".MAIN_DB_PREFIX."menu as m WHERE algorithm - direct and reverse. The first version proceeds from m.rowid = ".$_GET[’menuId’];» input blocks to the output, the second - goes in the reverse. The B285 = «$res = $db->query($sql);» basis is Ullmann’s algorithm [17, page 754]. Data received from the user is entered in $sql variable, and Direct version of the algorithm: the value of the variable without filtration is entered in SQL- OUT[INPUT] = 𝑣𝑖𝑛𝑝𝑢𝑡 ; request, which may lead to running of random SQL code. The For (each base block B, which differs from input) critical point is string B285; constant string is concatenated with OUT[B] = InitDataConst; taint data, and as a result the part of the string to the right of while (changes are entered in OUT) for (each basic block B, which differs from input) concatenation becomes taint. { IN[B] = ⋃P-predecessor OUT[P] ; 2. The use of passwords set directly in the software code OUT[B] = fB (IN[B]); is identified in AWCM project, in connect.php file: } Reverse version of the algorithm: B3 = «$db_hostname = "localhost";» IN[INPUT] = voutput; B4 = «$db_username = "root";» for(each basic block B, which differs from output) IN[B] = InitDataConst; B5 = «$db_userpass = "123456";» while (changes are entered in IN) for(each basic block B, which differs from output) B6 = «$db_database = "awcm";» { OUT[B] = ⋃P-predecessor B IN[P] ; B24 = «@mysql_connect($db_hostname, $db_username, $db_userpass);» IN[B] = fB (OUT[B]); } Parameters, including the password, set directly in the code, are used to connect to the database. The critical point is string Subject to [17], if algorithm converges, its result is the B24; in string B5 the right part of the expression is a constant; in solution to the dataflow problem. The obtained solution turns practice, the string is allocation of constant value to the variable out to be a so called maximum fixed point, which has the used further to set the password. Nowadays AppChecker, which property that in any other solution IN[B] and OUT[B] are implements algorithms of signature analysis using flow already present in this solution. If in this case the analysed block analysis, contains the total of 253 rules for the search of defects is final, the convergence of the algorithm is guaranteed. These in the software code in four programming languages: С/С++, statements are proved by Jeffrey Ullmann in [17, pages 754- Java, PHP, C#; the rules allow identifying 113 types of defects 755]. [28, 30]. AppChecker was tested in 90 projects with open source codes. It should be noted that in practice it is inadvisable to analyse all data used by the program. For example, if we consider X. CONCLUSION unfiltered user input as input data vinput, we are going to be The following conclusions can came from the results of the interested in B, where OUT[B] are entered in the database or study: output in HTML-context. Block B may also be represented by the function of the input information filtering, thus finalizing 1. Based on well-reputed signature analysis approach, the path and marking it as safe. the suggested method of the dataflow analysis can minimize the number of false positives and simplify the development of IX. EXAMPLES AND RESULTS signatures for an analyser production model. Dataflow analysis is widely spread in compilers and some 2. The suggested method and tools will be useful for the sort of program analysis tools in order to find mistakes, typos accredited testing laboratories as well as developers of safe and other accidentally inserted source code errors or software tools. Secure software development practices (we weaknesses. This paper is dedicated to the implementation and would, first of all, like to mention a recently approved national usage of well-known analysis approach for detecting potentially standard in this field [31-33]), are being implemented at a harmful code areas deliberately inserted into source code. The growing rate nowadays, therefore integration of the structured paper subject novelty is in joint usage dataflow and signature testing procedure in the process of the automated system template-based analysis for detection both embedded malicious development based on static signature analysis is a high-priority code (backdoors, trapdoors, hard-code credentials) and task. weaknesses caused by accidental developer's mistakes. Below are the examples of potentially harmful structures REFERENCES detected by the method described here using AppChecker [1] D.Yu. Volkanov, V.A. Zakharov, D.A. Zorin, V.V. Podymov, I.V. software. These examples are real but quite simple because we Konnov, “A Combined Toolset for the Verification of Real-Time Distributed Systems,” Program. Comput. Softw., vol. 41, no. 6, pp. think it is unacceptable to provide big and complex examples in 325-335, November 2015. DOI:10.1134/S0361768815060080. this article. 19 [2] I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. [18] A.S. Markov, A.A. Fadin, V.L. Tsirlov. “Multilevel Metamodel for Petrenko, and A. V. Khoroshilov, “Configurable toolset for static Heuristic Search of Vulnerabilities in the Software Source Code,” verification of operating systems kernel modules,” Program. Comput. International Journal of Control Theory and Applications. V. 9. N 30, pp. Softw., vol. 41, no. 1, pp. 49-64, January 2015. DOI: 313-320, December 2016. 10.1134/S0361768815010065. [19] M. Junker, R. Huuck, A. Fehnker, A. Knapp. “SMT-based false positive [3] I. S. Anureev, I.V Maryasov, and V.A. Nepomniaschy, “C-programs elimination in static program analysis,” Proceedings of 14th International verification based on mixed axiomatic semantics,” Autom. Control Conference on Formal Engineering Methods, Japan, Volume 7635 of Comput. Sci., vol. 45, no. 7, pp. 485-500, 2011. January 2012. LNCS. Springer, pp. 316-331, November 2012. DOI: 10.1007/978-3-642- [4] P. N. Devyanin, A. V Khoroshilov, V. V Kuliamin, A. K. Petrenko, and 34281-3_23. I. V Shchepetkov, “Formal Verification of OS Security Model with Alloy [20] W. Choi, S. Chandra, G. Necula, K. Sen. "SJS: A Type System for and Event-B BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z: JavaScript with Fixed Object Layout," International Static Analysis 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, Symposium, Static Analysis, pp. 181-198, September 2015. DOI: 2014. Proceedings,” Y. Ait Ameur and K.-D. Schewe, Eds. Berlin, 10.1007/978-3-662-48288-9_11. Heidelberg: Springer Berlin Heidelberg, 2014, pp. 309-313. [21] Z. Luo, T. Rezk, M. Serrano. “Automated code injection prevention for [5] D. Beyer and A. K. Petrenko, “Linux Driver Verification BT - Leveraging web applications,” Proceedings of the 2011 international conference Applications of Formal Methods, Verification and Validation. on Theory of Security and Applications, pp. 186-204, March 2011. Applications and Case Studies: 5th International Symposium, ISoLA DOI: 10.1007/978-3-642-27375-9_11. 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part [22] D. Ray, J. Ligatti. “Defining code-injection attacks,” Proceeding of the II,” T. Margaria and B. Steffen, Eds. Berlin, Heidelberg: Springer Berlin 39th annual ACM SIGPLAN-SIGACT symposium on Principles of Heidelberg, 2012, pp. 1-6. programming languages, pp. 179-190, January 2012. DOI: [6] E. di Bella, I. Fronza, N. Phaphoom, A. Sillitti, G. Succi, and J. Vlasenko, 10.1145/2103656.2103678. “Pair Programming and Software Defects--A Large, Industrial Case [23] S. Seo, A. Gupta, A. Sallam, E. Bertino, K. Yim. “Detecting mobile Study,” IEEE Transactions on Software Engineering, vol. 39, no. 7. pp. malware threats to homeland security through static analysis,” Journal of 930-953, Jul. 2013. Network and Computer Applications, vol: 38 (1) pp. 43-53, [7] S. M. Avdoshin and E. Y. Pesotskaya, “Software risk management,” 2011 February 2014. DOI: 10.1016/j.jnca.2013.05.008. 7th Central and Eastern European Software Engineering Conference [24] W. Lee, H. Oh, K. Yi. "A Progress Bar for Static Analyzers," International (CEE-SECR). pp. 1-6, 2011. Static Analysis Symposium, Static Analysis, pp. 184-200, [8] A. S. Kamkin and M. M. Chupilko, “Survey of modern technologies of September 2014, DOI: 10.1007/978-3-319-10936-7_12. simulation-based verification of hardware,” Program. Comput. Softw., [25] E. Goubault, S. Putot, F. Vedrine. "Modular static analysis with vol. 37, no. 3, pp. 147-152. May 2011. zonotopes," International Static Analysis Symposium, Static Analysis, [9] G. Reber, K. Malmquist, A. Shcherbakov. “Mapping the application pp. 24-40, September 2012. DOI: 10.1007/978-3-642-33125-1_5. security terrain,” Voprosy kiberbezopasnosti [Cybersecurity Issues], No [26] P. Calvert, A. Mycroft. "Control Flow Analysis for the Join Calculus," 1, pp. 36-39. January 2014. DOI: 10.21681/2311-3456-2014-2-36-39. International Static Analysis Symposium, Static Analysis, pp. 181-197, [10] A. Kozachok, M. Bochkov., T. M. Lai and E. Kochetkov. “First Order September 2012. DOI 10.1007/978-3-642-33125-1_14. Logic for Program Code Functional Requirements Description,” Voprosy [27] M. Madsen, A. Moller. "Sparse Dataflow Analysis with Pointers and kiberbezopasnosti [Cybersecurity issues]. No 3(21), pp. 2-7. August Reachability," International Static Analysis Symposium, Static Analysis, 2017. DOI: 10.21681/2311-3456-2017-3-2-7. pp. 201-218, September 2014. DOI: 10.1007/978-3-319-10936-7_13 [11] E. G. Vorobiev, S. A. Petrenko, I. V. Kovaleva, I. K. Abrosimov. [28] A. Markov, A. Fadin, A. Shvets, V. Tsirlov. “The experience of “Organization of the entrusted calculations in crucial objects of comparison of static security code analyzers,” International Journal of informatization under uncertainty,” The 20th IEEE International Advanced Studies, vol. 5. № 3. pp. 55-63, September 2015. Conference on Soft Computing and Measurements (SCM 2017), pp. 299 - 300. May 2017. DOI: 10.1109/SCM.2017.7970566. [29] D. Zhu, J. Jung, D. Song, T. Kohno, D. Wetherall “TaintEraser: protecting sensitive data leaks using application-level taint tracking,” Newsletter [12] A. Cox, B.-Y.E. Chang X. Rival. "Automatic Analysis of Open Objects ACM SIGOPS Operating Systems Review archive, January 2011, in Dynamic Language Programs," International Static Analysis Volume 45, Issue 1, pp. 142-154. DOI: 0.1145/1945023.1945039. Symposium, Static Analysis, pp. 134-150, September 2014. DOI: 10.1007/978-3-319-10936-7_9. [30] A. Barabanov, A. Markov, A. Fadin, V. Tsirlov. “Statistics of Software Vulnerabilities Detection During Certified Testing,” Voprosy [13] G. Balatsouras, Y. Smaragdakis. "Structure-Sensitive Points-To Analysis kiberbezopasnosti [Cybersecurity Issues]. No 2(20), pp. 2-8. May 2017. for C and C++", International Static Analysis Symposium, Static DOI: 10.21681/2311-3456-2017-2-2-8. Analysis, pp. 84-104, September 2016. DOI: 10.1007/978-3-662-53413- 7_5. [31] A. Barabanov, A. Markov, A. Fadin, V. Tsirlov, I. Shakhalov. “Synthesis of Secure Software Development Controls,” The 8th International [14] F. Zhu, J. Wei. “Static analysis based invariant detection for commodity Conference on Security of Information and Networks (Sochi, Russian operating systems,” Computers and Security, vol. 43, pp. 49-63, Federation, September 08-10, 2015). SIN ‘15. ACM New York, NY, June 2014. DOI: 10.1016/j.cose.2014.02.00. USA, pp. 93-97. September 08-10, 2015. DOI: [15] M. Bradley, F. Cassez, A. Fehnker, T. Given-Wilson, R. Huuck. “High 10.1145/2799979.2799998. performance Static Analysis for Industry,” Electronic Notes it Theoretical [32] A.V. Barabanov, A.S. Markov, V.L. Tsirlov. “Methodological Computer Science, vol. 289, pp. 3-14, December 2012. DOI: Framework for Analysis and Synthesis of a Set of Secure Software 10.1016/j.entcs.2012.11.002. Development Controls,” Journal of Theoretical and Applied Information [16] P. Gonzalez-de-Aledo, P. Sanchez, R. Huuck. "An Approach to Static- Technology. V. 88. No 1, pp. 77-88, June 2016. Dynamic Software Analysis," Proceedings of International Workshop on [33] A. Markov, A. Barabanov, V. Tsirlov V. Models for Testing Modifiable Formal Techniques for Safety-Critical Systems, pp. 225-240, November, Systems. In Book: Probabilistic Modeling in System Engineering, by ed. 2015. DOI: 10.1007/978-3-319-29510-7_13. Andrey Kostogryzov. InTech, 2018. [17] A.V. Aho, M.S. Lam, R. Sethi J.D. Ullman. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley; 2nd edition (September 10, 2006). 20