[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/349360.351130acmconferencesArticle/Chapter ViewAbstractPublication PagesfmspConference Proceedingsconference-collections
Article
Free access

Formal modeling of active network nodes using PVS

Published: 24 August 2000 Publication History

Abstract

Active Networks are a new type of networks where all elements are programmable. Active packets can contain fragments of code to be executed on intermediate nodes they pass through. Active nodes provide the necessary environment and resources for the packets to be processed. In giving the users the capability to program the network as they desire, there is an issue of security risks. This paper presents a formal model for an active node that can be used to specify and verify the correct operation of the node. The model is used to verify that scenarios where privacy of data is violated or functionality of a node is compromised never occur. The proposed model is generic to any type of active node and is written using the Prototype Verification System (PVS).

References

[1]
S. D. Alexander, W. A. Arbaugh, A. D. Keromytis, and J. M. Smith. A Secure Active Network Environment Architecture. IEEE Network, 1997.
[2]
W. A. Arbaugh, A. D. Keromytis, D. J. Farber, and J. M. Smith. Automated Recovery in a Secure Bootstrap Process. In Internet Society Symposium on Network and Distributed System Security, San Diago, CA, March 1998.
[3]
J. Crow, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS. SRIInternational, Menlo Park, CA, June 1995. Presented at WIFT'95.
[4]
G. Denker, J. Meseguer, and C. Talcott. Protocol specification and analysis in maude. In Workshop on Formal Methods and Security Protocols, June 1998.
[5]
A.N. O. W.Group.Nodeosinterface specification. http: //www.cs.princeton.edu/nsg/papers/nodeos.ps, July 23 1999.
[6]
A. N. O. W. Group and D. A. et al. Active network encapsulation protocol. http://www.cis.upenn.edu/~switchware/ANEP/, July 1997.
[7]
A. Kulkarni, G. Minden, and et al. Implementation of a prototype active network. In OPENARCH '98, San Francisco, CA, 1998.
[8]
I. Mutabanna. Exploring formal models for active network security. Master's thesis, The University of Cincinnati, 1999.
[9]
G. C. Necula. Proof-carrying code. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 15-17 1997.
[10]
U. of Cincinnati. Activespec website. http: //www.ececs.uc.edu/~kbse/projects/activespec/.
[11]
D. Rao, K. Swaminathan, R. Radhakrishnan, P. A. Wilsey, and P. Alexander. Anse: An active networks simulation environment. In Proceedings of Workshop on Distributed and Parallel Sysetms (DAPSYS 98), September 1998.
[12]
D. L. Tennenhouse, J. M. Smith, W. D. Sincoskie, D. J. Wetherall, and G. J. Minden. A Survey of Active Network Research. IEEE Communications Magazine, pages 80-86, January 1997.
[13]
D. L. Tennenhouse and D. J. Wetherall. Towards an Active Network Architecture. Computer Communication Review, 26(2):5-18, April 1996.
[14]
D. J. Wetherall, J. Guttag, and D. L. Tennenhouse. Ants: A toolkit for building and dynamically deploying network protocols. In IEEE OPENARCH'98, San Francisco, CA, April 1998.

Cited By

View all
  • (2017)A characterisation of verification tools for software defined networksJournal of Reliable Intelligent Environments10.1007/s40860-017-0045-y3:3(189-207)Online publication date: 29-Jul-2017
  • (2015)Model Checking Distributed Mandatory Access Control PoliciesACM Transactions on Information and System Security10.1145/278596618:2(1-25)Online publication date: 15-Jul-2015
  • (2012)Applying Formal Methods to Telecommunication Services with Active NetworksFormal Methods for Industrial Critical Systems10.1002/9781118459898.ch6(113-132)Online publication date: 29-Nov-2012
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
FMSP '00: Proceedings of the third workshop on Formal methods in software practice
August 2000
112 pages
ISBN:158113262X
DOI:10.1145/349360
Permission to make digital or hard copies of all or part 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 components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 August 2000

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

FMSP00
Sponsor:

Acceptance Rates

FMSP '00 Paper Acceptance Rate 9 of 31 submissions, 29%;
Overall Acceptance Rate 21 of 75 submissions, 28%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)22
  • Downloads (Last 6 weeks)2
Reflects downloads up to 31 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2017)A characterisation of verification tools for software defined networksJournal of Reliable Intelligent Environments10.1007/s40860-017-0045-y3:3(189-207)Online publication date: 29-Jul-2017
  • (2015)Model Checking Distributed Mandatory Access Control PoliciesACM Transactions on Information and System Security10.1145/278596618:2(1-25)Online publication date: 15-Jul-2015
  • (2012)Applying Formal Methods to Telecommunication Services with Active NetworksFormal Methods for Industrial Critical Systems10.1002/9781118459898.ch6(113-132)Online publication date: 29-Nov-2012
  • (2005)Integration of Reliability and Performance Analyses for Active Network ServicesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2004.08.066133(217-236)Online publication date: 1-May-2005
  • (2005)Model checking active networks with SPINComputer Communications10.1016/j.comcom.2004.08.00628:6(609-622)Online publication date: 1-Apr-2005

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media