Abstract
The financial technology sector is undergoing a transformation in moving to open-source and collaborative approaches as it works to address increasing compliance and assurance needs in its software stacks. Programming languages and validation technologies are a foundational part of this change. Based on this viewpoint, a consortium of leaders from Morgan Stanley and Goldman Sachs, researchers at Microsoft Research, and University College London, with support from the Fintech Open Source Foundation (FINOS) engaged to build an open programming stack to address these challenges.
The resulting stack, Morphir, centers around a converged core intermediate representation (IR), MorphirIR, that is a suitable target for existing languages in use in major investment banks and that is amenable to analysis with formal methods technologies. This paper documents the design of the MorphirIR language and the larger Morphir ecosystem with an emphasis on how they benefit from and enable formal methods for error checking and bug finding. We also report our initial experiences working in this system, our experience using formal validation in it, and identify open issues that we believe are important to the Fintech community and relevant to the research community.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
According to Thomson Reuters “Cost of Compliance 2021” \(78\%\) of market participants they surveyed expect the amount of regulatory information published by regulators and exchanges to increase in 2021.
References
AppInsights (2021). https://docs.microsoft.com/en-us/azure/azure-monitor/app/app-insights-overview
Barr, E.T., Vo, T., Le, V., Su, Z.: Automatic detection of floating-point exceptions. In: POPL (2013)
Bosque repository (2021). https://github.com/microsoft/BosqueLanguage
Dapr (2021). https://dapr.io/
de Moura, L., Bjørner, N., et al.: Z3 SMT Theorem Prover (2021). https://github.com/Z3Prover/z3
Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL 2011 (2011)
Fielding, R.T., Taylor, R.N.: Architectural styles and the design of network-based software architectures. Ph.D. thesis (2000)
Gallagher, K.B., Lyle, J.R.: Using program slicing in software maintenance. IEEE TSE 17 (1991)
Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39, 92–106 (2004)
Jiang, L., Su, Z.: Osprey: a practical type system for validating dimensional unit correctness of C programs. In: ICSE (2006)
Kirkegaard, C., Moller, A., Schwartzbach, M.I.: Static analysis of XML transformations in Java. IEEE TSE 30, 181–192 (2004)
Ko, A.J., Myers, B.A.: Designing the Whyline: a debugging interface for asking questions about program behavior. In: CHI (2004)
Complex Institution Liquidity Monitoring Report (2019). https://www.federalreserve.gov/reportforms/forms/FR_2052a20190331_f.pdf
Legend repository (2021). https://github.com/finos/legend
Marron, M., Kapur, D.: Comprehensive reachability refutation and witnesses generation via language and tooling co-design. Technical report MSR-TR-2021-17 (2021)
Marron, M., Stefanovic, D., Hermenegildo, M., Kapur, D.: Heap analysis in the presence of collection libraries. In: PASTE (2007)
Merigoux, D., Chataing, N., Protzenko, J.: A programming language for the law. In: ICFP, Catala (2021)
Morphir repository (2021). https://github.com/finos/morphir
O’Hearn, P.W.: Incorrectness logic. In: POPL (2019)
Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. PLDI (2015)
Passmore, G., et al.: The Imandra automated reasoning system (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 464–471. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_30
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21, 5–19 (2003)
Schelter, S., Lange, D., Schmidt, P., Celikel, M., Biessmann, F., Grafberger, A.: Automating large-scale data quality verification. Proc. VLDB Endow. 11, 1781–1794 (2018)
Smithy (2021). https://awslabs.github.io/smithy/
Solidity repository (2021). https://docs.soliditylang.org/
Yuan, D., Zheng, J., Park, S., Zhou, Y., Savage, S.: Improving software diagnosability via log enhancement. ASPLOS (2011)
Zakrzewski, J.: Towards verification of Ethereum smart contracts: a formalization of core of solidity. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 229–247. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03592-1_13
Acknowledgments
We would like to thank Beeke-Marie Nelke, Pierre De Belen, and Jianglai (Teddy) Zhang at Goldman Sachs for their technical contributions and feedback on this work. Thanks to our reviewers and numerous colleagues for their constructive comments and insights.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Goldbaum, S., Mihaly, A., Ellison, T., Barr, E.T., Marron, M. (2022). High Assurance Software for Financial Regulation and Business Platforms. In: Finkbeiner, B., Wies, T. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2022. Lecture Notes in Computer Science(), vol 13182. Springer, Cham. https://doi.org/10.1007/978-3-030-94583-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-94583-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-94582-4
Online ISBN: 978-3-030-94583-1
eBook Packages: Computer ScienceComputer Science (R0)