A semantic model of confinement and Locality theorem

Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similar...

Full description

Saved in:
Bibliographic Details
Published in:Frontiers of Computer Science 2010-03, Vol.4 (1), p.28-46
Main Authors: Wang, Shuling, Shu, Qin, Liu, Yijing, Qiu, Zongyan
Format: Article
Language:English
Subjects:
Computer Science
Confinement
Object oriented programming
Research Article
Semantics
Theorems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113
cites cdi_FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113
container_end_page 46
container_issue 1
container_start_page 28
container_title Frontiers of Computer Science
container_volume 4
creator Wang, Shuling
Shu, Qin
Liu, Yijing
Qiu, Zongyan
description Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μ Java, a subset of sequential Java that offers most object-oriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality theorem for checking well confinement of programs locally. By applying this theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.
doi_str_mv 10.1007/s11704-009-0075-6
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_crossref_primary_10_1007_s11704_009_0075_6</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2918720195</sourcerecordid><originalsourceid>FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113</originalsourceid><addsrcrecordid>eNp1kD1PwzAQhi0EEqXwA9giMQfunNiOx6riS6rEArPlxGdI1djFTof-e4ICYmI43Q3P-570MHaNcIsA6i4jKqhLAD2NEqU8YQuUqipVLeXp710JOGcXOW8BJOcSFqxeFZkGG8a-K4boaFdEX3Qx-D7QQGEsbHDFJnZ214_HYvygmGi4ZGfe7jJd_ewle3u4f10_lZuXx-f1alN2FcqxdChbVSE5DoJrx1vZ6kY4K5VHAklSOSUbz4Um4taDqLWuO9taLhpXIVZLdjP37lP8PFAezTYeUpheGq6xURxQi4nCmepSzDmRN_vUDzYdDYL5lmNmOWaSY77lGDll-JzJExveKf01_x_6Ak9NZWk</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2918720195</pqid></control><display><type>article</type><title>A semantic model of confinement and Locality theorem</title><source>Springer Nature</source><creator>Wang, Shuling ; Shu, Qin ; Liu, Yijing ; Qiu, Zongyan</creator><creatorcontrib>Wang, Shuling ; Shu, Qin ; Liu, Yijing ; Qiu, Zongyan</creatorcontrib><description>Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μ Java, a subset of sequential Java that offers most object-oriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality theorem for checking well confinement of programs locally. By applying this theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.</description><identifier>ISSN: 1673-7350</identifier><identifier>ISSN: 2095-2228</identifier><identifier>EISSN: 1673-7466</identifier><identifier>EISSN: 2095-2236</identifier><identifier>DOI: 10.1007/s11704-009-0075-6</identifier><language>eng</language><publisher>Heidelberg: SP Higher Education Press</publisher><subject>Computer Science ; Confinement ; Object oriented programming ; Research Article ; Semantics ; Theorems</subject><ispartof>Frontiers of Computer Science, 2010-03, Vol.4 (1), p.28-46</ispartof><rights>Higher Education Press and Springer Berlin Heidelberg 2010</rights><rights>Higher Education Press and Springer Berlin Heidelberg 2010.</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113</citedby><cites>FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,776,780,27903,27904</link.rule.ids></links><search><creatorcontrib>Wang, Shuling</creatorcontrib><creatorcontrib>Shu, Qin</creatorcontrib><creatorcontrib>Liu, Yijing</creatorcontrib><creatorcontrib>Qiu, Zongyan</creatorcontrib><title>A semantic model of confinement and Locality theorem</title><title>Frontiers of Computer Science</title><addtitle>Front. Comput. Sci. China</addtitle><description>Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μ Java, a subset of sequential Java that offers most object-oriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality theorem for checking well confinement of programs locally. By applying this theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.</description><subject>Computer Science</subject><subject>Confinement</subject><subject>Object oriented programming</subject><subject>Research Article</subject><subject>Semantics</subject><subject>Theorems</subject><issn>1673-7350</issn><issn>2095-2228</issn><issn>1673-7466</issn><issn>2095-2236</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2010</creationdate><recordtype>article</recordtype><recordid>eNp1kD1PwzAQhi0EEqXwA9giMQfunNiOx6riS6rEArPlxGdI1djFTof-e4ICYmI43Q3P-570MHaNcIsA6i4jKqhLAD2NEqU8YQuUqipVLeXp710JOGcXOW8BJOcSFqxeFZkGG8a-K4boaFdEX3Qx-D7QQGEsbHDFJnZ214_HYvygmGi4ZGfe7jJd_ewle3u4f10_lZuXx-f1alN2FcqxdChbVSE5DoJrx1vZ6kY4K5VHAklSOSUbz4Um4taDqLWuO9taLhpXIVZLdjP37lP8PFAezTYeUpheGq6xURxQi4nCmepSzDmRN_vUDzYdDYL5lmNmOWaSY77lGDll-JzJExveKf01_x_6Ak9NZWk</recordid><startdate>20100301</startdate><enddate>20100301</enddate><creator>Wang, Shuling</creator><creator>Shu, Qin</creator><creator>Liu, Yijing</creator><creator>Qiu, Zongyan</creator><general>SP Higher Education Press</general><general>Springer Nature B.V</general><scope>AAYXX</scope><scope>CITATION</scope><scope>8FE</scope><scope>8FG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>P5Z</scope><scope>P62</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope></search><sort><creationdate>20100301</creationdate><title>A semantic model of confinement and Locality theorem</title><author>Wang, Shuling ; Shu, Qin ; Liu, Yijing ; Qiu, Zongyan</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2010</creationdate><topic>Computer Science</topic><topic>Confinement</topic><topic>Object oriented programming</topic><topic>Research Article</topic><topic>Semantics</topic><topic>Theorems</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Wang, Shuling</creatorcontrib><creatorcontrib>Shu, Qin</creatorcontrib><creatorcontrib>Liu, Yijing</creatorcontrib><creatorcontrib>Qiu, Zongyan</creatorcontrib><collection>CrossRef</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central UK/Ireland</collection><collection>Advanced Technologies &amp; Aerospace Database‎ (1962 - current)</collection><collection>ProQuest Central Essentials</collection><collection>ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central Korea</collection><collection>ProQuest Central Student</collection><collection>SciTech Premium Collection</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>ProQuest advanced technologies &amp; aerospace journals</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><jtitle>Frontiers of Computer Science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Wang, Shuling</au><au>Shu, Qin</au><au>Liu, Yijing</au><au>Qiu, Zongyan</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>A semantic model of confinement and Locality theorem</atitle><jtitle>Frontiers of Computer Science</jtitle><stitle>Front. Comput. Sci. China</stitle><date>2010-03-01</date><risdate>2010</risdate><volume>4</volume><issue>1</issue><spage>28</spage><epage>46</epage><pages>28-46</pages><issn>1673-7350</issn><issn>2095-2228</issn><eissn>1673-7466</eissn><eissn>2095-2236</eissn><abstract>Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μ Java, a subset of sequential Java that offers most object-oriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality theorem for checking well confinement of programs locally. By applying this theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.</abstract><cop>Heidelberg</cop><pub>SP Higher Education Press</pub><doi>10.1007/s11704-009-0075-6</doi><tpages>19</tpages></addata></record>
fulltext fulltext
identifier ISSN: 1673-7350
ispartof Frontiers of Computer Science, 2010-03, Vol.4 (1), p.28-46
issn 1673-7350
2095-2228
1673-7466
2095-2236
language eng
recordid cdi_crossref_primary_10_1007_s11704_009_0075_6
source Springer Nature
subjects Computer Science
Confinement
Object oriented programming
Research Article
Semantics
Theorems
title A semantic model of confinement and Locality theorem
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-24T16%3A58%3A14IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=A%20semantic%20model%20of%20confinement%20and%20Locality%20theorem&rft.jtitle=Frontiers%20of%20Computer%20Science&rft.au=Wang,%20Shuling&rft.date=2010-03-01&rft.volume=4&rft.issue=1&rft.spage=28&rft.epage=46&rft.pages=28-46&rft.issn=1673-7350&rft.eissn=1673-7466&rft_id=info:doi/10.1007/s11704-009-0075-6&rft_dat=%3Cproquest_cross%3E2918720195%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c316t-d16b731ed20529d2b6b985da67f1e06e67d768f259ee2af054994caba258d3113%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2918720195&rft_id=info:pmid/&rfr_iscdi=true