Software engineers depend heavily on software libraries and have to update their dependencies once vulnerabilities are found in them. Software Composition Analysis (SCA) helps developers identify vulnerable libraries used by an application. A key challenge is the identification of libraries related to a given reported vulnerability in the National Vulnerability Database (NVD), which may not explicitly indicate the affected libraries. Recently, researchers have tried to address the problem of identifying the libraries from an NVD report by treating it as an extreme multi-label learning (XML) problem, characterized by its large number of possible labels and severe data sparsity. As input, the NVD report is provided, and as output, a set of relevant libraries is returned.

Software projects today rely on many third-party libraries, and therefore, are exposed to vulnerabilities in these libraries. When a library vulnerability is fixed, users are notified and advised to upgrade to a new version of the library. However, not all vulnerabilities are publicly disclosed, and users may not be aware of vulnerabilities that may affect their applications. Due to the above challenges, there is a need for techniques which can identify and alert users to silent fixes in libraries; commits that fix bugs with security implications that are not officially disclosed. We propose a machine learning approach to automatically identify vulnerability-fixing commits. Existing techniques consider only data within a commit, such as its commit message, which does not always have sufficiently discriminative information. To address this limitation, our approach incorporates the rich source of information from issue trackers. When a commit does not link to an issue, we use a commit-issue link recovery technique to infer the potential missing link. Our experiments are promising; incorporating information from issue trackers boosts the performance of a vulnerability-fixing commit classifier, improving over the strongest baseline by 11.1% on the entire dataset, which includes commits that do not link to an issue. On a subset of the data in which all commits explicitly link to an issue, our approach improves over the baseline by 12.5%.

Software composition analysis depends on database of open-source library vulerabilities, curated by security researchers using various sources, such as bug tracking systems, commits, and mailing lists. We report the design and implementation of a machine learning system to help the curation by by automatically predicting the vulnerability-relatedness of each data item. It supports a complete pipeline from data collection, model training and prediction, to the validation of new models before deployment. It is executed iteratively to generate better models as new input data become available. We use self-training to significantly and automatically increase the size of the training dataset, opportunistically maximizing the improvement in the models' quality at each iteration. We devised new deployment stability metric to evaluate the quality of the new models before deployment into production, which helped to discover an error. We experimentally evaluate the improvement in the performance of the models in one iteration, with 27.59% maximum PR AUC improvements. Ours is the first of such study across a variety of data sources. We discover that the addition of the features of the corresponding commits to the features of issues/pull requests improve the precision for the recall values that matter. We demonstrate the effectiveness of self-training alone, with 10.50% PR AUC improvement, and we discover that there is no uniform ordering of word2vec parameters sensitivity across data sources.

Software engineering practices have evolved to the point where a developer writing a new application today doesn’t start from scratch, but reuses a number of open source libraries and components. These third-party libraries evolve independently of the applications in which they are used, and may not maintain stable interfaces as bugs and vulnerabilities in them are fixed. This in turn causes API incompatibilities in downstream applications which must be manually resolved. Oversight here may manifest in many ways, from test failures to crashes at runtime. To address this problem, we present a static analysis for automatically and efficiently checking if a library upgrade introduces an API incompatibility.

The number of vulnerabilities in open source libraries is increasing rapidly. However, the majority of them do not go through public disclosure. These unidentified vulnerabilities put developers' products at risk of being hacked since they are increasingly relying on open source libraries to assemble and build software quickly. To find unidentified vulnerabilities in open source libraries and secure modern software development, we describe an efficient automatic vulnerability identification system geared towards tracking large-scale projects in real time using natural language processing and machine learning techniques. Built upon the latent information underlying commit messages and bug reports in open source projects using GitHub, JIRA, and Bugzilla, our K-fold stacking classifier achieves promising results on vulnerability identification. Compared to the state of the art SVM-based classifier in prior work on vulnerability identification in commit messages, we improve precision by 54.55% while maintaining the same recall rate. For bug reports, we achieve a much higher precision of 0.70 and recall rate of 0.71 compared to existing work. Moreover, observations from running the trained model at SourceClear in production for over 3 months has shown 0.83 precision, 0.74 recall rate, and detected 349 hidden vulnerabilities, proving the effectiveness and generality of the proposed approach.

HIPimm, an extension of the HIP/SLEEK automatic verification system, offers immutability guarantees on top of ensuring functional correctness for heap-manipulating programs. The extra capability of HIPimm, as compared to its precursor, is the ability to reason about immutability guarantees in a granular manner.For this purpose, we enhance the specification language with immutability annotations which provide the means to assert whether the annotated heap can be mutated or whether is inaccessible. As part of user defined predicates, these annotations are integrated at the data field level offering granular immutability guarantees. An immediate result of this new functionality is a finer level of precision in the verification process of programs involving heap data structures. That is, we enable the verification of program properties such as preservation of data structures shapes and/or values, flexible aliases, and information leakage prevention.

The use of formal methods for developing software is increasing. However in many cases only a model of the system is validated against a set of specifications. The actual implementation may thus not correspond to the formal model. One approach to this problem is to directly verify the actual implementation. Another solution is to provide a refinement scheme for the model. In this paper we present a method for refining a given Promela model to an implementation in C. We show that our refinement preserves the temporal properties (specified in LTL) of the original model. We give a new dual action semantics for a minimal core of Promela (called Featherweight Promela). The operational semantics of Featherweight Promela makes it easier to define the refinement calculus as a set of structural rules. Based on our calculus, we derive syntax directed translation rules for refinement of Promela models to C programs. These translation rules are easier to apply and generate an implementation which is a refinement of the formal model. We have applied our approach on existing Promela models and a larger case study of the cardiac pacemaker challenge.

To realize the potential of opportunistic and participatory sensing using mobile smartphones, a key challenge is ensuring the ease of developing and deploying such applications, without the need for the application writer to reinvent the wheel each time. To this end, we present a Platform for Remote Sensing using Smartphones (PRISM) that balances the interconnected goals of generality, security, and scalability. PRISM allows application writers to package their applications as executable binaries, which offers efficiency and also the flexibility of reusing existing code modules. PRISM then pushes the application out automatically to an appropriate set of phones based on a specified set of predicates. This push model enables timely and scalable application deployment while still ensuring a good degree of privacy. To safely execute untrusted applications on the smartphones, while allowing them controlled access to sensitive sensor data, we augment standard software sandboxing with several PRISM-specific elements like resource metering and forced amnesia.