Vulnerability impact analysis in software project dependencies based on Satisfiability Modulo Theories (SMT)

Software development projects are built on top of external libraries and tools that help manage code and databases and/or facilitate deployment. The external libraries that assist in these tasks create dependent relations with the developed software, thereby increasing the use of dependencies as a common practice. There exist mechanisms in the projects to set up software dependencies in terms of versions and restrictions between said projects. However, any problem, error, or vulnerability affecting a software's configuration dependencies can render the whole project vulnerable. This turns a secure dependency into an insecure dependency, and hinders the maintenance of security in software development projects, since current tools do not cover all possible configurations of dependencies. In this paper, our approach that enables the analysis and inference of the configuration of dependencies of projects in terms of potentially vulnerable configurations. The proposal is developed by constructing a dependency graph network attributed to vulnerabilities. Formal models are integrated based on Satisfiability Modulo Theories (SMT) to enable automatic analysis, such as the identification of the most secure configuration of dependencies. The automatic analysis facilitates ascertaining the vulnerability-free configurations of dependencies with maximum and minimum vulnerability impacts. This proposal has been evaluated by analysing more than 140 Python open-source code repositories and better results than other proposals have been achieved.