Ihor Kuz
Senior Research Engineer; Conjoint Senior Lecturer, UNSW

Publication List

Projects

Current Trustworthy Components eChronos Whole-System Assurance SMACCM

Past Security Architecture

Ihor leads the Systems Software team in the Trustworthy Systems group. The goal of this team is to investigate and develop safe and secure software that builds on seL4 and it's verified properties. A large part of this work is the development and maintenance of CAmkES (component architecture for microkernel-based embedded systems) , which provides a platform that enables the component-based design and implementation of modular, microkernel-based operating systems. Ihor also leads work in the Trustworthy Systems group on the design and development of the eChronos real-time operating system.

Collaborations

Ihor's past and present collaborations include:

• ETH Zurich
• Fraunhofer IESE
• VU Amstedam

Career Summary

Prior to joining Data61 (and previously NICTA), Ihor spent time as a research assistant and scientific programmer at the Vrije Universiteit, Amsterdam, designing and implementing the Globe wide-area distributed system. He was also a co-founder of Smarthaven, a startup company that developed intelligent mobile-agent based web search technology. In 2010/2011 Ihor spent a year in Europe, working on the Barrelfish multicore operating system at ETH Zurich, and on a version of AUTOSAR running on seL4 at Fraunhofer IESE.

Qualifications

In 1996, Ihor achieved a Masters degree in Computer Science from the Vrije Universiteit in Amsterdam, the Netherlands. Then, in 2003, he earned a PhD in Computer Science from the TU Delft in the Netherlands.

Affiliations

Ihor holds a conjoint appointment at UNSW with the School of Computer Science and Engineering where he teaches and supervises students.

Ihor is a member of the IEEE Computer Society, the ACM Special Interest Group in Operating Systems (SIGOPS), and USENIX.

Publications

• Google Scholar profile
• Best Papers
• Data61 Papers (To appear, 2017)
• NICTA Papers (2015, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2004)
• Research Theses Supervised

Best Papers

Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009

Data61 Papers

To appear

Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formal verification at scale Communications of the ACM

2017

Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson Secure mathematically-assured composition of control models Technical Report, Data61, CSIRO, September, 2017

NICTA Papers

2015

		Paul Rimba, Liming Zhu, Len Bass, Ihor Kuz and Steve Reeves Composing patterns to construct secure systems European Dependable Computing Conference, pp. 213–224, Paris, France, September, 2015
		Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015
		Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of RPC stub code International Symposium on Formal Methods, pp. 273–290, Oslo, Norway, June, 2015

2013

		Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013
		Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
		Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013

2012

		Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012
		Ihor Kuz, Liming Zhu, Len Bass, Mark Staples and Sherry Xu An architectural approach for cost effective trustworthy systems IEEE/IFIP Working Conference on Software Architecture (WICSA), pp. 325–328, Helsinki, Finland, August, 2012
		Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012

2011

Ihor Kuz, Zachary Anderson, Pravin Shinde and Timothy Roscoe Multicore OS benchmarks: we can do better Workshop on Hot Topics in Operating Systems, pp. 1–5, Napa, CA, USA, May, 2011

2010

		Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–10, Chicago, IL, USA, October, 2010
		Nicholas Fitzroy-Dale, Ihor Kuz and Gernot Heiser Architecture optimisation with Currawong Asia-Pacific Workshop on Systems (APSys), pp. 7–12, New Delhi, India, August, 2010
		Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker capDL: A language for describing capability-based systems Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010

2009

		Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
		Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser Dingo: Taming device drivers EuroSys Conference, pp. 275–288, Nuremberg, DE, April, 2009
		Nicholas Fitzroy-Dale and Ihor Kuz Towards automatic optimisation of componentised systems Workshop on Isolation and Integration in Embedded Systems, pp. 6, Nuremberg, Germany, March, 2009

2008

Ihor Kuz and Yan Liu Extending the capabilities of component models for embedded systems Third International Conference on the Quality of Software-Architectures (QoSA), pp. 182–196, Boston, MA, USA, January, 2008

2007

		Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
		Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces Workshop on Programming Languages and Operating Systems (PLOS), pp. 5, Stevenson, WA, USA, October, 2007
		Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols Workshop on Hot Topics in System Dependability, pp. Article 3, Edinburgh, UK, June, 2007
		Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser CAmkES: A component model for secure microkernel-based embedded systems Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, Volume 80, Number 5, pp. 687–699, May, 2007 Preprint

2006

Daniel Potts and Ihor Kuz Adapting distributed shared memory applications in diverse environments Proceedings of the 6th International Symposium on Cluster Computing and the Grid, Singapore, May, 2006

2004

		Frank Engel, Gernot Heiser, Ihor Kuz, Stefan M. Petters and Sergio Ruocco Operating systems on SoCs: A good idea? Embedded Real-Time Systems Implementation (ERTSI 2004) Workshop, Lisbon, Portugal, December, 2004
		Ihor Kuz L4 user manual — API version X.2 June, 2004

Research Theses Supervised

2016

Matthew Fernandez Formal verification of a component platform PhD Thesis, UNSW Computer Science & Engineering, Sydney, Australia, July, 2016

2011

Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011

2010

Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010

2008

Daniel Potts Eidolon: Adapting distributed applications to their environment PhD Thesis, UNSW, Sydney, Australia, January, 2008