Grants and Contributions:

Grant or Award spanning more than one fiscal year (2017-2018 to 2018-2019).

Ensuring that software is bug-free is a significant technical challenge, recognized as such in both industry and academic research. Exacerbating this challenge is the very real possibility that malicious parties can tease out and trigger bugs for personal and institutional gain. The technology of the company-partner for this proposal, nanopay, relates to the transfer of assets, for example, money. Their technology is a particularly attractive target for such malicious exploitation. Like most enterprises, nanopay invests considerably in technology and processes to ensure software quality. Of importance in this context is automation --- integration of automated testing in the process of developing and delivering software and related services. Existing solutions are severely lacking in this regard when it comes to security properties. In particular, as nanopay's solution is for asset-transfer, security in their context includes properties for that domain, for example, questions such as: Can a malicious user acquire an asset, yet not have paid for it?,' and,Can a malicious merchant somehow cheat a user out of payments, yet not deliver corresponding goods and services?' While there is broad research in frameworks for articulating security properties, and reasoning about them, automation of the nature we discuss above remains a long-term goal in research. There is no existing technology, of which were are aware, that nanopay can leverage in the near-term. The proposed work will train Highly Qualified Personnel (HQP) and be of short- and long-term value to industry in Ontario, Canada.