Andrew Martin : Publications

SoK: How Not to Architect Your Next−Generation TEE Malware?

Kubilay Ahmet Küçük‚ Steve Moyle‚ Andrew Martin‚ Alexandru Mereacre and Nicholas Allott

Pages 10. 2022.

Besides Intel's SGX technology‚ there are long−running discussions on how trusted computing technologies can be used to cloak malware. Past research showed example methods of malicious activities utilising Flicker‚ Trusted Platform Module‚ and recently integrating with enclaves. We observe two ambiguous methodologies of malware development being associated with SGX‚ and it is crucial to systematise their details. One methodology is to use the core SGX ecosystem to cloak malware; potentially affecting a large number of systems. The second methodology is to create a custom enclave not adhering to base assumptions of SGX‚ creating a demonstration code of malware behaviour with these incorrect assumptions; remaining local without any impact. We examine what malware aims to do in real−world scenarios and state−of−art techniques in malware evasion. We present multiple limitations of maintaining the SGX−assisted malware and evading it from anti−malware mechanisms. The limitations make SGX enclaves a poor choice for achieving a successful malware campaign. We systematise twelve misconceptions (myths) outlining how an overfit−malware using SGX weakens malware's existing abilities. We find the differences by comparing SGX assistance for malware with non−SGX malware (i.e.‚ malware in the wild in our paper). We conclude that the use of hardware enclaves does not increase the preexisting attack surface‚ enables no new infection vector‚ and does not contribute any new methods to the stealthiness of malware.

Details about SoK: How Not to Architect Your Next−Generation TEE Malware? | BibTeX data for SoK: How Not to Architect Your Next−Generation TEE Malware? | DOI (10.1145/3569562.3569568) | Link to SoK: How Not to Architect Your Next−Generation TEE Malware?

CRC: Fully General Model of Confidential Remote Computing

Kubilay Ahmet Küçük and Andrew Martin

In Open Access. 2021.

Digital services have been offered through remote systems for decades. The questions of how these systems can be built in a trustworthy manner and how their security properties can be understood are given fresh impetus by recent hardware developments‚ allowing a fuller‚ more general‚ exploration of the possibilities than has previously been seen in the literature. Drawing on and consolidating the disparate strains of research‚ technologies and methods employed throughout the adaptation of confidential computing‚ we present a novel‚ dedicated Confidential Remote Computing (CRC) model. CRC proposes a compact solution for next−generation applications to be built on strong hardware−based security primitives‚ control of secure software products' trusted computing base‚ and a way to make correct use of proofs and evidence reports generated by the attestation mechanisms. The CRC model illustrates the trade−offs between decentralisation‚ task size and transparency overhead. We conclude the paper with six lessons learned from our approach‚ and suggest two future research directions.

Details about CRC: Fully General Model of Confidential Remote Computing | BibTeX data for CRC: Fully General Model of Confidential Remote Computing | DOI (10.48550/arXiv.2104.03868) | Link to CRC: Fully General Model of Confidential Remote Computing

Managing confidentiality leaks throughprivate algorithms on Software Guard eXtensions (SGX) enclaves: Minimised TCB on secret−code execution with Early Private Mode (EPM)

K.A. Küçük‚ D. Grawrock and A.P. Martin

In EURASIP Journal on Information Security‚ Recent Advances in Software Security. Produced: 2017−2018. Received: 21 October 2018. Accepted: 03 May 2019. Published: 05 September 2019. Springer Nature.. 2019.

Many applications are built upon private algorithms‚ and executing them in untrusted‚ remote environments poses confidentiality issues. To some extent‚ these problems can be addressed by ensuring the use of secure hardware in the execution environment; however‚ an insecure software−stack can only provide limited algorithm secrecy. This paper aims to address this problem‚ by exploring the components of the Trusted Computing Base (TCB) in hardware−supported enclaves. First‚ we provide a taxonomy and give an extensive understanding of trade−offs during secure enclave development. Next‚ we present a case study on existing secret−code execution frameworks; which have bad TCB design due to processing secrets with commodity software in enclaves. This increased attack surface introduces additional footprints on memory that breaks the confidentiality guarantees; as a result‚ the private algorithms are leaked. Finally‚ we propose an alternative approach for remote secret−code execution of private algorithms. Our solution removes the potentially untrusted commodity software from the TCB and provides a minimal loader for secret−code execution. Based on our new enclave development paradigm‚ we demonstrate three industrial templates for cloud applications: ① computational power as a service‚ ② algorithm querying as a service‚ and ③ data querying as a service. Keywords: Trusted Computing Base (TCB)‚ Software Guard eXtensions (SGX) Enclave‚ Private Algorithms‚ Secret−Code Execution (SCE)‚ Algorithm Owner (AO)‚ Hardware Owner (HO)‚ Data Owner (DO)‚ Enclave Developer’s (ED) Responsibilities‚ Side−Channels‚ Early Private Mode (EPM)‚ Protected Code Creator (PCC)‚ Protected Code Loader (PCL)‚ Internal Enclave Functions (IEF)‚ Public Internal Enclave Functions (PIEF)‚ Serialised Secret Internal Enclave Functions (SSIEF).

Details about Managing confidentiality leaks throughprivate algorithms on Software Guard eXtensions (SGX) enclaves: Minimised TCB on secret−code execution with Early Private Mode (EPM) | BibTeX data for Managing confidentiality leaks throughprivate algorithms on Software Guard eXtensions (SGX) enclaves: Minimised TCB on secret−code execution with Early Private Mode (EPM) | DOI (10.1186/s13635-019-0091-5) | Link to Managing confidentiality leaks throughprivate algorithms on Software Guard eXtensions (SGX) enclaves: Minimised TCB on secret−code execution with Early Private Mode (EPM)

White−Stingray: Evaluating IMSI Catchers Detection Applications

Ravishankar Borgaonkar‚ Shinjo Park‚ Altaf Shaik‚ Andrew Martin and Jean−Pierre Seifert

In 11th USENIX Workshop on Offensive Technologies (WOOT 17). 2017.

Details about White−Stingray: Evaluating IMSI Catchers Detection Applications | BibTeX data for White−Stingray: Evaluating IMSI Catchers Detection Applications | Download PublicationFile of White−Stingray: Evaluating IMSI Catchers Detection Applications | Download PublicationFile of White−Stingray: Evaluating IMSI Catchers Detection Applications

Exploring the use of Intel SGX for Secure Many−Party Applications

K.A. Küçük‚ A. Paverd‚ A. Martin‚ N. Asokan‚ A. Simpson and R. Ankele

In Proceedings of the 1st Workshop on System Software for Trusted Execution (SysTEX '16). New York‚ NY‚ USA. 2016. ACM.

The theoretical construct of a Trusted Third Party (TTP) has the potential to solve many security and privacy challenges. In particular‚ a TTP is an ideal way to achieve secure multiparty computation—a privacy−enhancing technique in which mutually distrusting participants jointly compute a function over their private inputs without revealing these inputs. Although there exist cryptographic protocols to achieve this‚ their performance often limits them to the two−party case‚ or to a small number of participants. However‚ many real−world applications involve thousands or tens of thousands of participants. Examples of this type of many−party application include privacy−preserving energy metering‚ location−based services‚ and mobile network roaming. Challenging the notion that a trustworthy TTP does not exist‚ recent research has shown how trusted hardware and remote attestation can be used to establish a sufficient level of assurance in a real system such that it can serve as a trustworthy remote entity (TRE). We explore the use of Intel SGX‚ the most recent and arguably most promising trusted hardware technology‚ as the basis for a TRE for many−party applications. Using privacy−preserving energy metering as a case study‚ we design and implement a prototype TRE using SGX‚ and compare its performance to a previous system based on the Trusted Platform Module (TPM). Our results show that even without specialized optimizations‚ SGX provides comparable performance to the optimized TPM system‚ and therefore has significant potential for large−scale many−party applications.

Details about Exploring the use of Intel SGX for Secure Many−Party Applications | BibTeX data for Exploring the use of Intel SGX for Secure Many−Party Applications | DOI (10.1145/3007788.3007793) | Link to Exploring the use of Intel SGX for Secure Many−Party Applications

Applying the Trustworthy Remote Entity to Privacy−Preserving Multiparty Computation: Requirements and Criteria for Large−Scale Applications

R. Ankele‚ K.A. Küçük‚ A.P. Martin‚ A.C. Simpson and A. Paverd

In Proceedings of the 13th IEEE International Conference on Advanced and Trusted Computing (ATC 2016). 2016.

The significant improvements in technology that have been seen in recent years have resulted in a shift in the computing paradigm: from isolated computational tasks to distributed tasks executed in multi−party settings. Secure Multi−Party Computation (MPC) allows for multiple parties to jointly compute a function on their private inputs. Unfortunately‚ traditional MPC algorithms are inefficient in the presence of a large number of participants. Moreover‚ in the traditional setting‚ MPC is only concerned with privacy of the input values. However‚ there is often a need to preserve the privacy of individuals on the basis of the output of the computation. Techniques proposed by the Trusted Computing community have shown promise in the context of new secure‚ efficient large−scale applications. In this paper‚ we define‚ analyse several use cases related to large−scale applications of the MPC paradigm. From these use cases‚ we derive requirements‚ criteria to evaluate certain MPC protocols used for large−scale applications. Furthermore‚ we propose the utilisation of a Trustworthy Remote Entity‚ privacy−preserving algorithms to achieve confidentiality‚ privacy in such settings.

Details about Applying the Trustworthy Remote Entity to Privacy−Preserving Multiparty Computation: Requirements and Criteria for Large−Scale Applications | BibTeX data for Applying the Trustworthy Remote Entity to Privacy−Preserving Multiparty Computation: Requirements and Criteria for Large−Scale Applications | DOI (10.1109/UIC-ATC-ScalCom-CBDCom-IoP-SmartWorld.2016.0077) | Link to Applying the Trustworthy Remote Entity to Privacy−Preserving Multiparty Computation: Requirements and Criteria for Large−Scale Applications

Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing

Andrew J Paverd‚ Andrew P Martin and Ian Brown

In Fifth IEEE International Conference on Smart Grid Communications (SmartGridComm 2014). 2014.

Details about Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing | BibTeX data for Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing | Download Paverd-SmartGridComm-2014.pdf of Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing | Download Paverd-SmartGridComm-2014-slides.pdf of Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing | DOI (10.1109/SmartGridComm.2014.7007758) | Link to Privacy−Enhanced Bi−Directional Communication in the Smart Grid using Trusted Computing

Security and Privacy in Smart Grid Demand Response Systems

Andrew Paverd‚ Andrew Martin and Ian Brown

In Second Open EIT ICT Labs Workshop on Smart Grid Security − SmartGridSec14. 2014.

Details about Security and Privacy in Smart Grid Demand Response Systems | BibTeX data for Security and Privacy in Smart Grid Demand Response Systems | Download  (pdf) of Security and Privacy in Smart Grid Demand Response Systems

Security and Privacy in Smart Grid Demand Response Systems

Andrew J Paverd‚ Andrew P Martin and Ian Brown

In Jorge Cuellar, editor, Smart Grid Security. Pages 1−15. Springer International Publishing. 2014.

Details about Security and Privacy in Smart Grid Demand Response Systems | BibTeX data for Security and Privacy in Smart Grid Demand Response Systems | Download  (pdf) of Security and Privacy in Smart Grid Demand Response Systems | DOI (10.1007/978-3-319-10329-7_1) | Link to Security and Privacy in Smart Grid Demand Response Systems

Hardware Security for Device Authentication in the Smart Grid

Andrew Paverd and Andrew Martin

In First Open EIT ICT Labs Workshop on Smart Grid Security − SmartGridSec12. Berlin‚ Germany. 2012.

Details about Hardware Security for Device Authentication in the Smart Grid | BibTeX data for Hardware Security for Device Authentication in the Smart Grid | Download  (pdf) of Hardware Security for Device Authentication in the Smart Grid | Link to Hardware Security for Device Authentication in the Smart Grid

BottleCap: a Credential Manager for Capability Systems

Justin King−Lacroix and Andrew Martin

In Proceedings of The Seventh ACM Workshop on Scalable Trusted Computing. 2012.

To appear

Details about BottleCap: a Credential Manager for Capability Systems | BibTeX data for BottleCap: a Credential Manager for Capability Systems

Provenance as a Security Control

Andrew Martin‚ John Lyle and Cornelius Namiluko

In Proceedings of TaPP'12: the 4th USENIX Workshop on the Theory and Practice of Provenance. USENIX. 2012.

Details about Provenance as a Security Control | BibTeX data for Provenance as a Security Control | Link to Provenance as a Security Control

On the design and development of webinos: a distributed mobile application middleware

John Lyle‚ Shamal Faily‚ Ivan Flechais‚ Andre Paul‚ Ayse Goker‚ Hans Myrhaug‚ Heiko Desruelle and Andrew Martin

In Proceedings of the 12th IFIP WG 6.1 international conference on Distributed applications and interoperable systems. Pages 140–147. 2012.

Details about On the design and development of webinos: a distributed mobile application middleware | BibTeX data for On the design and development of webinos: a distributed mobile application middleware | Download  (pdf) of On the design and development of webinos: a distributed mobile application middleware

Provenance−Based Model for Verifying Trust−Properties

Cornelius Namiluko and Andrew Martin

In Stefan Katzenbeisser‚ Edgar Weippl‚ L. Camp‚ Melanie Volkamer‚ Mike Reiter and Xinwen Zhang, editors, TRUST AND TRUSTWORTHY COMPUTING. Vol. 7344/2012 of Lecture Notes in Computer Science. Pages 255−272. Springer Berlin / Heidelberg. 2012.

Details about Provenance−Based Model for Verifying Trust−Properties | BibTeX data for Provenance−Based Model for Verifying Trust−Properties | DOI (10.1007/978-3-642-30921-2_15) | Link to Provenance−Based Model for Verifying Trust−Properties

Secure Virtual Layer Management of Clouds

Imad M. Abbadi‚ Muntaha Alawneh and Andrew Martin

In The 10th IEEE International Conference on Trust‚ Security and Privacy in Computing and Communications (IEEE TrustCom−11). IEEE. November, 2011.

Details about Secure Virtual Layer Management of Clouds | BibTeX data for Secure Virtual Layer Management of Clouds

Trustworthy Middleware Services in the Cloud

Imad M. Abbadi‚ Mina Deng‚ Marco Nalin‚ Andrew Martin‚ Milan Petkovic‚ Ilaria Baroni and Alberto Sanna

In CloudDB'11. ACM Press‚ NY. October, 2011.

Details about Trustworthy Middleware Services in the Cloud | BibTeX data for Trustworthy Middleware Services in the Cloud

Trust in Clouds

Imad Abbadi and Andrew Martin

In Elsevier Information Security Technical Report. Vol. to appear. 2011.

Details about Trust in Clouds | BibTeX data for Trust in Clouds

A Survey of Trust in Workflows and Relevant Contexts

W. Viriyasitavat and A. Martin

In Communications Surveys Tutorials‚ IEEE. Vol. PP. No. 99. Pages 1 −30. 2011.

Details about A Survey of Trust in Workflows and Relevant Contexts | BibTeX data for A Survey of Trust in Workflows and Relevant Contexts | DOI (10.1109/SURV.2011.072811.00081)

Verifying Trustworthiness of Virtual Appliances in Collaborative Environments

Cornelius Namiluko‚ Jun Ho Huh and Andrew Martin

2011.

Details about Verifying Trustworthiness of Virtual Appliances in Collaborative Environments | BibTeX data for Verifying Trustworthiness of Virtual Appliances in Collaborative Environments

Formalizing Trust Requirements and Specification in Service Workflow Environments.

Wattana Viriyasitavat and Andrew Martin

In Runtong Zhang‚ Jos� Cordeiro‚ Xuewei Li‚ Zhenji Zhang and Juliang Zhang, editors, ICEIS (3). Pages 196−206. SciTePress. 2011.

Details about Formalizing Trust Requirements and Specification in Service Workflow Environments. | BibTeX data for Formalizing Trust Requirements and Specification in Service Workflow Environments. | Link to Formalizing Trust Requirements and Specification in Service Workflow Environments.

Achieving attestation with less effort: an indirect and configurable approach to integrity reporting

Jun Ho Huh‚ Hyoungshick Kim‚ John Lyle and Andrew Martin

In Proceedings of the sixth ACM workshop on Scalable trusted computing. Pages 31–36. ACM. 2011.

Details about Achieving attestation with less effort: an indirect and configurable approach to integrity reporting | BibTeX data for Achieving attestation with less effort: an indirect and configurable approach to integrity reporting | DOI (10.1145/2046582.2046589) | Link to Achieving attestation with less effort: an indirect and configurable approach to integrity reporting

In the Relation of Workflow and Trust Characteristics‚ and Requirements in Service Workflows

Wattana Viriyasitavat and Andrew Martin

In Abd Manaf‚ Azizah‚ Akram Zeki‚ Mazdak Zamani‚ Suriayati Chuprat and Eyas El−Qawasmeh, editors, Informatics Engineering and Information Science. Vol. 251 of Communications in Computer and Information Science. Pages 492−506. Springer Berlin Heidelberg. 2011.

10.1007/978−3−642−25327−0_42

Details about In the Relation of Workflow and Trust Characteristics‚ and Requirements in Service Workflows | BibTeX data for In the Relation of Workflow and Trust Characteristics‚ and Requirements in Service Workflows | Link to In the Relation of Workflow and Trust Characteristics‚ and Requirements in Service Workflows

Engineering Attestable Services (short paper)

John Lyle and Andrew Martin

In Ahmad−Reza Acquisti Alessandro; Smith Sean W.; Sadeghi, editor, Proceedings of the 3rd International Conference on Trust and Trustworthy Computing. Pages 257–264. Springer. June, 2010.

Details about Engineering Attestable Services (short paper) | BibTeX data for Engineering Attestable Services (short paper) | Download  (pdf) of Engineering Attestable Services (short paper) | DOI (10.1007/978-3-642-13869-0) | Link to Engineering Attestable Services (short paper)

A Multiple Comparative Study of Test−With Development Product Changes and their Effects on Team Speed and Product Quality

Steve Bannerman and Andrew Martin

No. RR−10−03. April, 2010.

Details about A Multiple Comparative Study of Test−With Development Product Changes and their Effects on Team Speed and Product Quality | BibTeX data for A Multiple Comparative Study of Test−With Development Product Changes and their Effects on Team Speed and Product Quality | Download  (pdf) of A Multiple Comparative Study of Test−With Development Product Changes and their Effects on Team Speed and Product Quality

A multiple comparative study of test−with development product changes and their effects on team speed and product quality

Steve Bannerman and Andrew Martin

In Empirical Software Engineering. 2010.

Details about A multiple comparative study of test−with development product changes and their effects on team speed and product quality | BibTeX data for A multiple comparative study of test−with development product changes and their effects on team speed and product quality | DOI (10.1007/s10664-010-9137-5) | Link to A multiple comparative study of test−with development product changes and their effects on team speed and product quality

Managing application whitelists in trusted distributed systems

Jun Ho Huh‚ John Lyle‚ Cornelius Namiluko and Andrew Martin

In Future Generation Computer Systems. Vol. In Press‚ Accepted Manuscript. 2010.

Details about Managing application whitelists in trusted distributed systems | BibTeX data for Managing application whitelists in trusted distributed systems | DOI (DOI: 10.1016/j.future.2010.08.014) | Link to Managing application whitelists in trusted distributed systems

Trusted Computing and Provenance: Better Together

John Lyle and Andrew Martin

In Proceedings of the 2nd Workshop on the Theory and Practice of Provenance. Usenix. 2010.

Details about Trusted Computing and Provenance: Better Together | BibTeX data for Trusted Computing and Provenance: Better Together | Download  (pdf) of Trusted Computing and Provenance: Better Together | Download (pdf) of Trusted Computing and Provenance: Better Together

Towards a Trustable Virtual Organisation

Jun Ho Huh and Andrew Martin

Pages 425−431. Los Alamitos‚ CA‚ USA. November, 2009. IEEE Computer Society.

Details about Towards a Trustable Virtual Organisation | BibTeX data for Towards a Trustable Virtual Organisation | DOI (10.1109/ISPA.2009.72)

On the Feasibility of Remote Attestation for Web Services

John Lyle and Andrew Martin

In SecureCom09: Proceedings of the International Symposium on Secure Computing. Pages 283−288. IEEE. 2009.

Details about On the Feasibility of Remote Attestation for Web Services | BibTeX data for On the Feasibility of Remote Attestation for Web Services | Download PublicationFile of On the Feasibility of Remote Attestation for Web Services | Download feasibility-ieee.pdf of On the Feasibility of Remote Attestation for Web Services | Link to On the Feasibility of Remote Attestation for Web Services

The Ten Page Introduction to Trusted Computing

Andrew Martin

No. RR−08−11. OUCL. December, 2008.

Details about The Ten Page Introduction to Trusted Computing | BibTeX data for The Ten Page Introduction to Trusted Computing | Download of The Ten Page Introduction to Trusted Computing

Trusted Logging for Grid Computing

Jun Ho Huh and Andrew Martin

In Third Asia−Pacific Trusted Infrastructure Technologies Conference. Pages 30−42. Los Alamitos‚ CA‚ USA. October, 2008. IEEE Computer Society.

Details about Trusted Logging for Grid Computing | BibTeX data for Trusted Logging for Grid Computing | DOI (10.1109/APTC.2008.9)

Association of parameter‚ software‚ and hardware variation with large−scale behavior across 57‚000 climate models

Christopher G. Knight‚ Sylvia H. E. Knight‚ Neil Massey‚ Tolu Aina‚ Carl Christensen‚ Dave J. Frame‚ Jamie A. Kettleborough‚ Andrew Martin‚ Stephen Pascoe‚ Ben Sanderson‚ David A. Stainforth and Myles R. Allen

In Proceedings of the National Academy of Sciences in the United States of America. Vol. 104. No. 30. Pages 12259–12264. July, 2007.

Details about Association of parameter‚ software‚ and hardware variation with large−scale behavior across 57‚000 climate models | BibTeX data for Association of parameter‚ software‚ and hardware variation with large−scale behavior across 57‚000 climate models | DOI (10.1073/pnas.0608144104)

Data access and analysis with distributed federated data servers in climateprediction.net

N. Massey‚ T. Aina‚ M. Allen‚ C. Christensen‚ D. Frame‚ D. Goodman‚ J Kettleborough‚ A. Martin‚ S. Pascoe and D. Stainforth

In Advances in Geosciences. Vol. 8. Pages 49–56. June, 2006.

Details about Data access and analysis with distributed federated data servers in climateprediction.net | BibTeX data for Data access and analysis with distributed federated data servers in climateprediction.net | Download (pdf) of Data access and analysis with distributed federated data servers in climateprediction.net

Preface.

Alvaro E. Arenas‚ Jin Song Dong‚ Andrew Martin and Brian Matthews

In Electr. Notes Theor. Comput. Sci.. Vol. 151. No. 2. Pages 1. 2006.

Details about Preface. | BibTeX data for Preface.

Innovations for Grid Security from Trusted Computing

Wenbo Mao‚ Andrew Martin‚ Hai Jin and Huanguo Zhang

In Fourteenth International Workshop on Security Protocols. Springer−Verlag. 2006.

To appear

Details about Innovations for Grid Security from Trusted Computing | BibTeX data for Innovations for Grid Security from Trusted Computing

Towards a Secure‚ Tamper−Proof Grid Platform.

Andrew Cooper and Andrew Martin

In Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2006)‚ 16−19 May 2006‚ Singapore. Pages 373−380. IEEE Computer Society. 2006.

Details about Towards a Secure‚ Tamper−Proof Grid Platform. | BibTeX data for Towards a Secure‚ Tamper−Proof Grid Platform.

ShibGrid: Shibboleth Access for the UK National Grid Service

David Spence‚ Neil Geddes‚ Jens Jensen‚ Andrew Richards‚ Matthew Viljoen‚ Andrew Martin‚ Matthew Dovey‚ Mark Norman‚ Kang Tang‚ Anne Trefethen‚ David Wallom‚ Rob Allan and David Meredith

In eScience 2006‚ Amsterdam. 2006.

Details about ShibGrid: Shibboleth Access for the UK National Grid Service | BibTeX data for ShibGrid: Shibboleth Access for the UK National Grid Service

Trusted Delegation for Grid Computing

Andrew Cooper and Andrew Martin

In The Second Workshop on Advances in Trusted Computing. 2006.

Details about Trusted Delegation for Grid Computing | BibTeX data for Trusted Delegation for Grid Computing

Towards an open‚ trusted digital rights management platform

Andrew Cooper and Andrew Martin

In DRM '06: Proceedings of the ACM workshop on Digital rights management. Pages 79–88. New York‚ NY‚ USA. 2006. ACM Press.

Details about Towards an open‚ trusted digital rights management platform | BibTeX data for Towards an open‚ trusted digital rights management platform | DOI (http://doi.acm.org/10.1145/1179509.1179525)

Editorial‚ Guest Editors‚ Special issue on Grid Security

Howard Chivers and Andrew Martin

In Software—Practice and Experience. Vol. 35. No. 9. July, 2005.

Details about Editorial‚ Guest Editors‚ Special issue on Grid Security | BibTeX data for Editorial‚ Guest Editors‚ Special issue on Grid Security

Scientific middleware for abstracted parallelisation

Daniel Goodman

No. RR−05−07. Oxford University Computing Laboratory. November, 2005.

Details about Scientific middleware for abstracted parallelisation | BibTeX data for Scientific middleware for abstracted parallelisation

Uncertainty in the predictions of the climate response to rising levels of greenhouse gases

D. A. Stainforth‚ T. Aina‚ C. Christensen‚ M. Collins‚ N. Faull‚ D. J. Frame‚ J. A. Kettleborough‚ S. Knight‚ A. Martin‚ J. M. Murphy‚ C. Piani‚ D. Sexton‚ L. A. Smith‚ R. A. Spicer‚ A. J. Thorpe and M. R. Allen

In Nature. Vol. 433. No. 7024. Pages 403–406. January, 2005.

Details about Uncertainty in the predictions of the climate response to rising levels of greenhouse gases | BibTeX data for Uncertainty in the predictions of the climate response to rising levels of greenhouse gases | DOI (10.1038/nature03301)

A Taxonomy of Web Services Using CSP

Lee Momtahan‚ Andrew Martin and A. W. Roscoe

In Proceedings of Web Languages and Formal Methods. 2005.

Details about A Taxonomy of Web Services Using CSP | BibTeX data for A Taxonomy of Web Services Using CSP

On two kinds of public−resource distributed computing

Andrew Martin‚ Tolu Aina‚ Carl Christensen‚ Jamie Kettleborough and David Stainforth

In Proceedings of Fourth UK e−Science All Hands Meeting. 2005.

Details about On two kinds of public−resource distributed computing | BibTeX data for On two kinds of public−resource distributed computing

Object Models: Job Submission in DataGrids

Lee Momtahan and Andrew Martin

No. RR−04−26. Oxford University Computing Laboratory. February, 2004.

Details about Object Models: Job Submission in DataGrids | BibTeX data for Object Models: Job Submission in DataGrids | Download  (pdf) of Object Models: Job Submission in DataGrids

A taxonomy of web services using CSP

Lee Momtahan‚ Andrew Martin and A. W. Roscoe

No. RR−04−22. Oxford University Computing Laboratory. October, 2004.

Details about A taxonomy of web services using CSP | BibTeX data for A taxonomy of web services using CSP | Download  (ps) of A taxonomy of web services using CSP

Teaching Formal Methods in Context

Jim Davies‚ Andrew Simpson and Andrew Martin

In C. Neville Dean and Raymond T. Boute, editors, Symposium on Teaching Formal Methods. Vol. 3294 of Lecture Notes in Computer Science. Springer−Verlag. 2004.

Details about Teaching Formal Methods in Context | BibTeX data for Teaching Formal Methods in Context

Grid Style Web Services for ClimatePrediction.net

Daniel Goodman and Andrew Martin

In S. Newhouse and S. Parastatidis, editors, GGF workshop on building Service−Based Grids‚ Honolulu‚ Hawaii. Global Grid Forum. 2004.

Details about Grid Style Web Services for ClimatePrediction.net | BibTeX data for Grid Style Web Services for ClimatePrediction.net

Grids and Private Networks are Anthitetical

Andrew Martin and Carl Cook

In Howard Chivers and Andrew Martin, editors, Grid Security Practice and Experience Workshop. Computer Science Department‚ University of York‚ YCS−2004−380. 2004.

Details about Grids and Private Networks are Anthitetical | BibTeX data for Grids and Private Networks are Anthitetical

Security Principles for Public−Resource Modeling Research.

Dave Stainforth‚ Andrew Martin‚ Andrew Simpson‚ Carl Christensen‚ Jamie Kettleborough‚ Tolu Aina and Myles Allen

In 13th IEEE International Workshops on Enabling Technologies (WETICE 2004)‚ Infrastructure for Collaborative Enterprises‚ 14−16 June 2004‚ Modena‚ Italy. Pages 319−324. IEEE Computer Society. 2004.

Details about Security Principles for Public−Resource Modeling Research. | BibTeX data for Security Principles for Public−Resource Modeling Research.

A Critical Survey of Grid Security Requirements and Technologies

Philippa J. Broadfoot and Andrew P. Martin

No. RR−03−15. Oxford University Computing Laboratory. August, 2003.

Details about A Critical Survey of Grid Security Requirements and Technologies | BibTeX data for A Critical Survey of Grid Security Requirements and Technologies | Download  (ps.gz) of A Critical Survey of Grid Security Requirements and Technologies

Supplementing the understanding of Z: a formal approach to database design

A. C. Simpson and A. P. Martin

In Proceedings of the BCS Teaching Formal Methods workshop. BCS. 2003.

Details about Supplementing the understanding of Z: a formal approach to database design | BibTeX data for Supplementing the understanding of Z: a formal approach to database design

On the supervision and assessment of part−time postgraduate software engineering projects

A C. Simpson‚ A. P. Martin‚ J. Gibbons‚ J. W. Davies and S. W. McKeever

In Proceedings of the 25th International Conference on Software Engineering (ICSE)‚ Portland‚ Oregon‚ 3–10 May‚ 2003. Pages 628–633. IEEE Computer Society Press. 2003.

Details about On the supervision and assessment of part−time postgraduate software engineering projects | BibTeX data for On the supervision and assessment of part−time postgraduate software engineering projects

ZML: XML Support for Standard Z

Mark Utting‚ Ian Toyn‚ Jing Sun‚ Andrew Martin‚ Jin Song Dong‚ Nicholas Daley and David W. Currie

In Didier Bert‚ Jonathan P. Bowen‚ Steve King and Marina Waldén, editors, ZB 2003: Formal Specification and Development in Z and B‚ Third International Conference of B and Z Users‚ Turku‚ Finland‚ June 4−6‚ 2003‚ Proceedings. Vol. 2651 of Lecture Notes in Computer Science. Pages 437−456. Springer. 2003.

Details about ZML: XML Support for Standard Z | BibTeX data for ZML: XML Support for Standard Z

On The Supervision and Assessment Of Part−Time Postgraduate Software Engineering Projects.

Andrew Simpson‚ Andrew Martin‚ Jeremy Gibbons‚ Jim Davies and Steve McKeever

In Proceedings of the 25th International Conference on Software Engineering‚ May 3−10‚ 2003‚ Portland‚ Oregon‚ USA. Pages 628−633. IEEE Computer Society. 2003.

Details about On The Supervision and Assessment Of Part−Time Postgraduate Software Engineering Projects. | BibTeX data for On The Supervision and Assessment Of Part−Time Postgraduate Software Engineering Projects.

Generalizing the Schema Calculus: Database Schemas and Beyond

Andrew Martin and Andrew Simpson

In Proceedings of 10th Asia−Pacific Software Engineering Conference. IEEE press. 2003.

to appear

Details about Generalizing the Schema Calculus: Database Schemas and Beyond | BibTeX data for Generalizing the Schema Calculus: Database Schemas and Beyond

Grid Security: Requirements and Technologies A Survey of the State−of−the−art

Philippa Broadfoot and Andrew Martin

No. PRG−RR−03−15. Programming Research Group. Oxford University Computing Laboratory‚ Wolfson Building‚ Parks Road‚ Oxford‚ OX1 3QD‚ UK. 2003.

Details about Grid Security: Requirements and Technologies A Survey of the State−of−the−art | BibTeX data for Grid Security: Requirements and Technologies A Survey of the State−of−the−art

climateprediction.com: security and design planning

D. Stainforth‚ J. A. Kettleborough‚ A. P. Martin‚ A. C. Simpson‚ A. P. Martin‚ R. Gillis‚ A. Akkas‚ R. Gault‚ M. Collins‚ D. J. Gavaghan and M. Allen

In Proceedings of the 2002 UK e−Science All Hands Meeting. 2002.

Details about climateprediction.com: security and design planning | BibTeX data for climateprediction.com: security and design planning

Climateprediction.net: design principles for public resource modelling research.

D. Stainforth‚ J. Kettleborough‚ A. Martin‚ A. Simpson‚ R. Gillis‚ A. Akkas‚ R. Gault‚ M. Collins‚ D. Gavaghan and M. Allen

In Proc. 14th IASTED conference on parallel and distributed computing systems.. Pages 32–38. 2002.

Details about Climateprediction.net: design principles for public resource modelling research. | BibTeX data for Climateprediction.net: design principles for public resource modelling research.

e−Science Experiences: Software Engineering Practice and the EU DataGrid

Lee Momtahan and Andrew Martin

In Proc. Asia−Pacific Software Engineering Conference. Pages 269–275. IEEE Press. 2002.

Details about e−Science Experiences: Software Engineering Practice and the EU DataGrid | BibTeX data for e−Science Experiences: Software Engineering Practice and the EU DataGrid

e−Science: A Software Engineering Challenge

Andrew Martin and Lee Momtahan

Poster. 2002.

UK eScience All Hands Meeting

Details about e−Science: A Software Engineering Challenge | BibTeX data for e−Science: A Software Engineering Challenge

Lifting in Z

A. Martin and C. Fidge

In Proceedings of CATS'2001. No. 42. 2001.

Details about Lifting in Z | BibTeX data for Lifting in Z

Relating Z and First−order logic

A. P. Martin

In Formal Aspects of Computing. Vol. 12. Pages 199–209. 2000.

Details about Relating Z and First−order logic | BibTeX data for Relating Z and First−order logic

A Calculus for Schemas in Z

S. M. Brien and A. P. Martin

In J. Symbolic Computation. Vol. 30. No. 1. Pages 63–91. 2000.

Details about A Calculus for Schemas in Z | BibTeX data for A Calculus for Schemas in Z

Declarative languages in education

H. Glaser‚ P. H. Hartel‚ M. Leuschel and A. Martin

In Encyclopaedia of Microcomputers. Vol. 27. Pages 79–102. Marcel Dekker Inc., New York. 2000.

Details about Declarative languages in education | BibTeX data for Declarative languages in education

Relating Z and first−order logic

Andrew Martin

In Jeanette M. Wing‚ Jim Woodcock and Jim Davies, editors, FM'99 – Formal Methods. No. 1708‚1709. Pages 1266–1280. Springer−Verlag. September, 1999.

Details about Relating Z and first−order logic | BibTeX data for Relating Z and first−order logic

Questions and Answers About Ten Formal Methods

P. Hartel‚ M. Butler‚ A. Currie‚ P. Henderson‚ M. Leuschel‚ A. Martin‚ A. Smith‚ U. Ultes−Nitsche and B. Walters

In S. Gnesi and D. Latella, editors, Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems. Vol. II. Pages 179−203. Trento‚ Italy. July, 1999. ERCIM. STAR/CNR‚ Pisa‚ Italy.

Details about Questions and Answers About Ten Formal Methods | BibTeX data for Questions and Answers About Ten Formal Methods

Applying the Cogito Program Development Environment to Real−Time System Design

C. J. Fidge‚ P. Kearney and A. P. Martin

In C. McDonald, editor, Computer Science '98. Pages 367–378. Springer−Verlag. 1998.

Proc. 21st Australasian Computer Science Conference‚ Perth‚ 4−6 February 1998. Australian Computer Science Communications‚ Vol. 20‚ No. 1. Also available as technical report SVRC−TR−97−36.

Details about Applying the Cogito Program Development Environment to Real−Time System Design | BibTeX data for Applying the Cogito Program Development Environment to Real−Time System Design | Link to Applying the Cogito Program Development Environment to Real−Time System Design

A Set−Theoretic Model for Real−Time Specification and Reasoning

C. J. Fidge‚ I. J. Hayes‚ A. P. Martin and A. K. Wabenhorst

In J. Jeuring, editor, Mathematics of Program Construction (MPC'98). Vol. 1422 of Lecture Notes in Computer Science. Pages 188–206. Springer−Verlag. 1998.

Details about A Set−Theoretic Model for Real−Time Specification and Reasoning | BibTeX data for A Set−Theoretic Model for Real−Time Specification and Reasoning

A Tactic Language for Ergo

A. Martin‚ R. Nickson and M. Utting

In Lindsay Groves and Steve Reeves, editors, Formal Methods Pacific '97. Singapore. July, 1997. Springer−Verlag.

Also appears as TR97−16‚ Software Verification Research Centre‚ The University of Queensland‚ QLD 4072‚ Australia

Details about A Tactic Language for Ergo | BibTeX data for A Tactic Language for Ergo

W Reconstructed

Jon Hall and Andrew Martin

In Jonathan P. Bowen‚ Michael G Hinchey and David Till, editors, ZUM'97: The Z Formal Specification Notation‚ 10th International Conference of Z Users‚ Reading‚ UK‚ April 1997‚ Proceedings. Vol. 1212 of Lecture Notes in Computer Science. Berlin Heidelberg. April, 1997. Springer−Verlag.

Details about W Reconstructed | BibTeX data for W Reconstructed

The Cogito development system

Owen Traynor‚ Dan Hazel‚ Peter Kearney‚ Andrew Martin‚ Ray Nickson and Luke Wildman

In Michael Johnson, editor, Algebraic Methodology and Software Technology. Vol. 1349 of LNCS. Pages 586–591. Berlin. December, 1997. Springer−Verlag.

6th International conference‚ AMAST'97‚ Sydney‚ Australia

Details about The Cogito development system | BibTeX data for The Cogito development system

Improving Angel's Parallel Operator: Gumtree's Approach

Andrew Martin‚ Ray Nickson and Mark Utting

No. 97−15. Software Verification Research Centre. The University of Queensland‚ QLD 4072‚ Australia. 1997.

Details about Improving Angel's Parallel Operator: Gumtree's Approach | BibTeX data for Improving Angel's Parallel Operator: Gumtree's Approach

Why effective proof tool support for Z is hard

Andrew Martin

No. 97−34. Software Verification Research Centre. 1997.

Details about Why effective proof tool support for Z is hard | BibTeX data for Why effective proof tool support for Z is hard | Link to Why effective proof tool support for Z is hard

A Tactic Calculus

A. P. Martin‚ P. H. B. Gardiner and J. C. P. Woodcock

In Formal Aspects of Computing. Vol. 8. No. 4. Pages 479–489. 1996.

An abridged version appears in the printed journal; the full version is available in the electronic supplement to Formal Aspects of Computing‚ 8E‚ pp244–285. http://link.springer.de/link/service/journals/00165/supp/list94_96.htm

Details about A Tactic Calculus | BibTeX data for A Tactic Calculus

Infinite Lists for Specifying Functional Programs in Z

Andrew Martin

In Proceedings of Australian Refinement Workshop. University of Queensland. 1996.

Details about Infinite Lists for Specifying Functional Programs in Z | BibTeX data for Infinite Lists for Specifying Functional Programs in Z | Link to Infinite Lists for Specifying Functional Programs in Z

Of Tactics and Monads

Andrew Philip Martin

1996.

Work in progress

Details about Of Tactics and Monads | BibTeX data for Of Tactics and Monads

A Tutorial on Proof in Standard Z

Stephen M. Brien and Andrew P. Martin

No. PRG−120. Programming Research Group‚ Oxford University Computing Laboratory. Wolfson Building‚ Parks Road‚ Oxford‚ OX1 3QD‚ UK. 1995.

Presented at ZUM'95

Details about A Tutorial on Proof in Standard Z | BibTeX data for A Tutorial on Proof in Standard Z

Machine−Assisted Theorem−Proving for Software Engineering

Andrew Martin

PhD Thesis , type= D.Phil. Thesis. University of Oxford. 1994.

Also available as Technical Monograph PRG−121‚ ISBN 0−902928−95−3‚ Oxford University Computing Laboratory‚ Wolfson Building‚ Parks Road‚ Oxford‚ OX1 3QD‚ UK

Details about Machine−Assisted Theorem−Proving for Software Engineering | BibTeX data for Machine−Assisted Theorem−Proving for Software Engineering

Encoding : A Logic for Z in 2OBJ

Andrew Martin

In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: Industrial−Strength Formal Methods. Vol. 670 of Lecture Notes in Computer Science. Pages 462–481. Springer−Verlag. 1993.

Details about Encoding : A Logic for Z in 2OBJ | BibTeX data for Encoding : A Logic for Z in 2OBJ

Infinite Lists in Z

Andrew Martin

1993.

Draft paper

Details about Infinite Lists in Z | BibTeX data for Infinite Lists in Z

Soundness of an Encoding of A Logic for Z in 2OBJ

Hendrik Hilberdink and Andrew Martin

OUCL(PRG). June, 1992.

Details about Soundness of an Encoding of A Logic for Z in 2OBJ | BibTeX data for Soundness of an Encoding of A Logic for Z in 2OBJ

A Monadic Interpretation of Tactics

Andrew Martin and Jeremy Gibbons

Submitted to MPC2002

Details about A Monadic Interpretation of Tactics | BibTeX data for A Monadic Interpretation of Tactics