skip to main content
10.1145/2993600.2993604acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
short-paper
Open access

Short Paper: Rusty Types for Solid Safety

Published: 24 October 2016 Publication History

Abstract

Programs operating "close to the metal" necessarily handle memory directly. Because of this, they must be written in languages like C or C++. These languages lack any kind of guarantee on memory or race safety, often leading to security vulnerabilities and unreliable software. Ideally, we would like a practical language that gives programmers direct control over memory and aliasing while also offering race and memory safety guarantees. We present Rusty Types and an accompanying type system, inspired by the Rust language, that enable memory-safe and race-free references through ownership and restricted aliasing in the type system. In this paper, we formally describe a small subset of the syntax, semantics, and type system of Metal, our Rust-based language that enjoys Rusty Types. Our type system models references and ownership as capabilities, where bindings have indirect capabilities on value locations. We also present speculative extensions to Rusty Types that allow greater flexibility in single threaded programs while maintaining the same guarantees.

References

[1]
J. Aldrich and C. Chambers. Ownership Domains: Separating Aliasing Policy from Mechanism, pages 1--25. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.
[2]
J. Aldrich, V. Kostadinov, and C. Chambers. Alias annotations for program understanding. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '02, pages 311--330, New York, NY, USA, 2002. ACM.
[3]
P. S. Almeida. Balloon types: Controlling sharing of state in data types, pages 32--59. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997.
[4]
K. Bierho and J. Aldrich. Modular typestate checking of aliased objects. In Proceedings of the 22Nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications, OOPSLA '07, pages 301--320, New York, NY, USA, 2007. ACM.
[5]
H.-J. Boehm. Destructors, nalizers, and synchronization. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '03, pages 262--272, New York, NY, USA, 2003. ACM.
[6]
C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '02, pages 211--230, New York, NY, USA, 2002. ACM.
[7]
C. Boyapati, B. Liskov, and L. Shrira. Ownership types for object encapsulation. SIGPLAN Not., 38(1):213--223, Jan. 2003.
[8]
J. Boyland. Alias burying: Unique variables without destructive reads. Softw. Pract. Exper., 31(6):533--553, May 2001.
[9]
J. Boyland. Checking interference with fractional permissions. In Proceedings of the 10th International Conference on Static Analysis, SAS'03, pages 55--72, Berlin, Heidelberg, 2003. Springer-Verlag.
[10]
J. T. Boyland and W. Retert. Connecting effects and uniqueness with adoption. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, pages 283--295, New York, NY, USA, 2005. ACM.
[11]
N. R. Cameron, S. Drossopoulou, J. Noble, and M. J. Smith. Multiple ownership. SIGPLAN Not., 42(10):441--460, Oct. 2007.
[12]
D. Clarke and S. Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. SIGPLAN Not., 37(11):292--310, Nov. 2002.
[13]
D. G. Clarke, J. Noble, and J. Potter. Simple ownership types for object containment. In Proceedings of the 15th European Conference on Object-Oriented Programming, ECOOP '01, pages 53--76, London, UK, UK, 2001. Springer-Verlag.
[14]
D. G. Clarke, J. M. Potter, and J. Noble. Ownership types for flexible alias protection. In Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '98, pages 48--64, New York, NY, USA, 1998. ACM.
[15]
K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '99, pages 262--275, New York, NY, USA, 1999. ACM.
[16]
D. Cunningham, W. Dietl, S. Drossopoulou, A. Francalanza, P. Muller, and A. J. Summers. Formal methods for components and objects. chapter Universe Types for Topology and Encapsulation, pages 72--112. Springer-Verlag, Berlin, Heidelberg, 2008.
[17]
R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, PLDI '01, pages 59--69, New York, NY, USA, 2001. ACM.
[18]
M. Fahndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI '02, pages 13--24, New York, NY, USA, 2002. ACM.
[19]
S. Heule, K. R. M. Leino, P. Muller, and A. J. Summers. Fractional permissions without the fractions. In Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, FTfJP '11, pages 1:1--1:6, New York, NY, USA, 2011. ACM.
[20]
M. Hicks, G. Morrisett, D. Grossman, and T. Jim. Experience with safe manual memory-management in cyclone. In Proceedings of the 4th International Symposium on Memory Management, ISMM '04, pages 73--84, New York, NY, USA, 2004. ACM.
[21]
J. Hogg. Islands: Aliasing protection in object-oriented languages. In Conference Proceedings on Object-oriented Programming Systems, Languages, and Applications, OOPSLA '91, pages 271--285, New York, NY, USA, 1991. ACM.
[22]
B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for c and java. In Proceedings of the Third International Conference on NASA Formal Methods, NFM'11, pages 41--55, Berlin, Heidelberg, 2011. Springer-Verlag.
[23]
N. H. Minsky. Towards alias-free pointers. In Proceedings of the 10th European Conference on Object-Oriented Programming, ECCOP '96, pages 189--209, London, UK, UK, 1996. Springer-Verlag.
[24]
G. Morrisett, A. Ahmed, and M. Fluet. L3: A linear language with locations. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, TLCA'05, pages 293--307, Berlin, Heidelberg, 2005. Springer-Verlag.
[25]
P. Muller and A. Rudich. Ownership transfer in universe types. In Proceedings of the 22Nd Annual ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications, OOPSLA '07, pages 461--478, New York, NY, USA, 2007. ACM.
[26]
K. Naden, R. Bocchino, J. Aldrich, and K. Bierho. A type system for borrowing permissions. SIGPLAN Not., 47(1):557--570, Jan. 2012.
[27]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02, pages 55--74, Washington, DC, USA, 2002. IEEE Computer Society.
[28]
Rust Project Developers. The Rust Programming Language, 2016.
[29]
F. Smith, D. Walker, and G. Morrisett. Alias Types, pages 366--381. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000.
[30]
M. Tofte and J.-P. Talpin. Region-based memory management. Inf. Comput., 132(2):109--176, Feb. 1997.
[31]
J. Vitek and B. Bokowski. Confined types. SIGPLAN Not., 34(10):82--96, Oct. 1999.
[32]
P. Wadler. Linear types can change the world! In IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 347--359. North Holland, 1990.
[33]
D. Walker and G. Morrisett. Alias Types for Recursive Data Structures, pages 177--206. Springer Berlin Heidelberg, Berlin, Heidelberg, 2001.

Cited By

View all
  • (2024)Point Intervention: Improving ACVP Test Vector Generation Through Human Assisted FuzzingInformation and Communications Security10.1007/978-981-97-8801-9_3(43-62)Online publication date: 27-Aug-2024
  • (2021)Translating C to safer RustProceedings of the ACM on Programming Languages10.1145/34854985:OOPSLA(1-29)Online publication date: 15-Oct-2021

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
October 2016
116 pages
ISBN:9781450345743
DOI:10.1145/2993600
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2016

Check for updates

Author Tags

  1. alias types
  2. aliasing
  3. capabilities
  4. concurrency
  5. formalization
  6. linear types
  7. memory safety
  8. ownership types
  9. race safety
  10. rust
  11. rusty types
  12. semantics
  13. syntax
  14. type system

Qualifiers

  • Short-paper

Conference

CCS'16
Sponsor:

Acceptance Rates

PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;
Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)222
  • Downloads (Last 6 weeks)34
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Point Intervention: Improving ACVP Test Vector Generation Through Human Assisted FuzzingInformation and Communications Security10.1007/978-981-97-8801-9_3(43-62)Online publication date: 27-Aug-2024
  • (2021)Translating C to safer RustProceedings of the ACM on Programming Languages10.1145/34854985:OOPSLA(1-29)Online publication date: 15-Oct-2021

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media