Complete Publications

Journal Publications

hicks-02-19-08.bib

@article{TCWHM08,
  author = {Patrick Traynor and Michael Chien and Scott Weaver and Boniface Hicks and Patrick McDaniel},
  date-added = {2008-02-19 08:16:45 -0500},
  date-modified = {2008-02-19 08:16:45 -0500},
  journal = {{ACM Transactions on Information and System Security (TISSEC)}},
  number = {3},
  title = {{Non-Invasive Methods for Host Certification}},
  volume = {11},
  year = {2008}
}

@article{FHW00, abstract = {

This paper presents a demand transformation analysis that maps a predicate's output demands to its input demands. This backward dataflow analysis for concurrent constraint programs is constructed in the framework of abstract interpretation. In the context of stream parallelism, this analysis identifies an amount of input data for which predicate execution can safely wait without danger of introducing deadlock. We assume that programs are well-moded and prove that our analysis is safe. We have constructed an implementation of this analysis and tested it on some small, illustrative programs and have determined that it gives useful results in practice. We identify several applications of the analysis results to distributed implementations of concurrent constraint languages, including thread construction and communication granularity. This analysis will enable exisiting computation cost estimation analyses to be applied to stream-parallel logic languages.

}, author = {Moreno Falaschi and Patrick Hicks and William Winsborough}, journal = {Journal of Logic Programming}, month = mar, number = 3, pages = {185--215}, pdf = {papers/demandTransformAnalysis.pdf}, title = {Demand Transformation Analysis for Concurrent Constraint Programs}, volume = 41, year = 2000 }

@article{HH00, abstract = {

We present a formal specification of unCurrying for a higher-order, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions that are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function, rather than only unCurrying all of a function's parameters. We present the specification as a deductive system that axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, that implements unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a richer form of unCurrying than is currently found in compilers for functional languages.

}, author = {John Hannan and Patrick Hicks}, journal = {Journal of Higher Order and Symbolic Computation}, number = 3, pages = {179--216}, pdf = {papers/HOUncurryingJournal.pdf}, title = {Higher-Order Uncurrying}, volume = 13, year = 2000 }

Conference and Workshop Publications

hicks-02-19-08.bib

@inproceedings{HKM07,
  abstract = {Security-typed languages such as Jif require the programmer to label variables 
with information flow security policies as part of application development. The 
compiler then flags errors wherever information leaks may occur. Resolving 
these information leaks is a critical task in security-typed language 
application development. Unfortunately, because information flows can be quite 
subtle, simple error messages tend to be insufficient for finding and resolving 
the source of information leaks; more sophisticated development tools are 
needed for this task. To this end we provide a set of principles to guide the 
development of such tools. Furthermore, we implement a subset of these 
principles in an integrated development environment (IDE) for Jif, called 
Jifclipse, which is built on the Eclipse extensible development platform. Our 
plug-in provides a Jif programmer with additional tools to view hidden 
information generated by a Jif compilation, to suggest fixes for errors, and to 
get more specific information behind an error message.  Better development tools
are essential for making security-typed application development practical;
Jifclipse is a first step in this process.},
  address = {San Diego, CA},
  author = {Boniface Hicks and Dave King and Patrick McDaniel},
  booktitle = {Proceedings of the 2nd ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS '07)},
  date-added = {2008-02-19 09:00:54 -0500},
  date-modified = {2008-02-19 09:01:14 -0500},
  editor = {Michael Hicks},
  month = {June 14},
  pdf = {papers/hicks-plas07jifclipse.pdf},
  publisher = {ACM Press},
  title = {Jifclipse: Development Tools for Security-Typed Applications},
  url = {http://doi.acm.org/10.1145/1255329.1255331},
  year = {2007}
}

@inproceedings{HRJ+07a,
  abstract = {Recent advances in the area of security-typed languages have enabled the
development of
realistic applications aware of information flow security. Traditionally, operating systems have
enforced MAC with minimal dependence on application programs.
Although these approaches have common goals, they have progressed
independently.  However, there are many cases where systems depend on
user-level programs to enforce information flows, so integration of
information flow enforcement between the operating systems and
security-typed applications would be beneficial.  In this paper, we
examine what it takes to integrate information flow enforcement of a
security-typed extension of Java with SELinux.  We find that SELinux
has most of the necessary features to build a proof-of-concept system,
but other services are necessary, such as verifying compliance between
information flow policies.  Ultimately, we are optimistic that the
comprehensive access control enforcement of SELinux will be ideal for
integration with these security-typed applications.},
  address = {Baltimore, MD, USA},
  author = {Boniface Hicks and Sandra Rueda and Trent Jaeger and Patrick McDaniel},
  booktitle = {Proceedings of the 3rd {SEL}inux Symposium},
  date-added = {2008-02-19 08:40:50 -0500},
  date-modified = {2008-02-19 08:44:19 -0500},
  keywords = {Information Flow Policies, Java Information Flow (Jif), security-typed languages, SELinux},
  month = {March},
  pdf = {papers/hicks-selinux07integrating.pdf},
  title = {Integrating SELinux with Security-typed Languages},
  url = {http://selinux-symposium.org/2007/papers/12-integrating.pdf},
  year = {2007}
}

@inproceedings{HRJ+07b,
  abstract = {Commercial operating systems have recently 
introduced mandatory access controls (MAC) that can be 
used to ensure system-wide data confidentiality and in- 
tegrity. These protections rely on restricting the flow of 
information between processes based on security levels. 
The problem is, there are many applications that defy sim- 
ple classification by security level, some of them essential 
for system operation. Surprisingly, the common practice 
among these operating systems is simply to mark these 
applications as ``trusted'', and thus allow them to bypass 
label protections. This compromise is not a limitation 
of MAC or the operating system services that enforce it, 
but simply a fundamental inability of any operating sys- 
tem to reason about how applications treat sensitive data 
internally---and thus the OS must either restrict the data 
that they receive or trust them to handle it correctly. 
These practices were developed prior to the advent 
security-typed languages. These languages provide a 
means of reasoning about how the OS's sensitive data is 
handled within applications. Thus, applications can be 
shown to enforce system security by guaranteeing, in ad- 
vance of execution, that they will adhere to the OS's MAC 
policy. In this paper, we provide an architecture for an op- 
erating system service, that integrate security-typed lan- 
guage with operating system MAC services. We have built 
an implementation of this service, called SIESTA, which 
handles applications developed in the security-typed lan- 
guage, Jif, running on the SELinux operating system. We 
also provide some sample applications to demonstrate the 
security, flexibility and efficiency of our approach.},
  address = {Santa Clara, CA, USA},
  author = {Boniface Hicks and Sandra Rueda and Trent Jaeger and Patrick McDaniel},
  booktitle = {Proceedings of the {USENIX} Annual Technical Conference},
  date-added = {2008-02-19 08:39:26 -0500},
  date-modified = {2008-02-19 08:44:08 -0500},
  month = {June},
  pdf = {papers/hicks-usenix07selinuxJif.pdf},
  title = {From Trusted to Secure: Building and Executing Applications that Enforce System Security},
  url = {http://www.usenix.org/events/usenix07/tech/hicks.html},
  year = {2007}
}

@inproceedings{HRS+07,
  abstract = {The SELinux mandatory access control (MAC) policy has recently added a
multi-level security (MLS) model which is able to express a fine
granularity of control over a subject's access rights.  The problem
is that the richness of this policy makes it impractical to verify, by hand,
that a given policy has certain important information flow properties or is
compliant
with another policy.  To address this, we have modeled the SELinux MLS policy
using a logical specification and implemented that specification in the Prolog
language.  Furthermore, we have developed some analyses for testing the
properties of a given policy as well an algorithm to determine whether one
policy is compliant with another.  We have implemented these analyses in Prolog
and compiled our implementation into a tool for SELinux MLS policy analysis,
called \tool.  Using \tool, we verified some important properties of the
SELinux MLS reference policy,
namely that it satisfies the simple security condition and $\star$-property
defined by Bell and LaPadula},
  address = {Antipolis, France},
  author = {Boniface Hicks and Sandra Rueda and St. Clair, Luke and Trent Jaeger and Patrick McDaniel},
  booktitle = {Proceedings of the {ACM} Symposium on Access Control Models and Technologies ({SACMAT})},
  date-added = {2008-02-19 08:35:13 -0500},
  date-modified = {2008-02-19 08:44:00 -0500},
  month = {June},
  pdf = {papers/hicks-sacmat07mls-semantics.pdf},
  title = {A Logical Specification and Analysis for {SELinux} {MLS} Policy},
  url = {http://doi.acm.org/10.1145/1266840.1266854},
  year = {2007}
}

@inproceedings{HMM07,
  abstract = {Security-typed languages (STLs) are powerful tools for
provably implementing policy in applications. The programmer
maps policy onto programs by annotating types
with information flow labels, and the STL compiler guarantees
that data always obeys its label as it flows within an
application. As data flows into or out of an application,
however, a runtime system is needed to mediate between
the information flow world within the application and the
non-information flow world of the operating system. In the
few existing STL applications, this problem has been handled
in ad hoc ways that hindered software engineering and
security analysis. In this paper, we present a principled approach
to STL runtime system development along with policy
infrastructure and class abstractions for the STL, Jif,
that implement these principles. We demonstrate the effectiveness
of our approach by using our infrastructure to
develop a firewall application, FlowWall, that provably
enforces its policy.},
  address = {Miami, Fl},
  author = {Boniface Hicks and Timothy Misiak and Patrick McDaniel},
  booktitle = {23rd Annual Computer Security Applications Conference (ACSAC)},
  date-added = {2008-02-19 08:23:59 -0500},
  date-modified = {2008-02-19 08:24:29 -0500},
  month = {December},
  pdf = {papers/hicks-acsac07channels.pdf},
  title = {Channels: Runtime System Infrastructure for Security-typed Languages},
  url = {http://www.ieeexplore.ieee.org/iel5/4412959/4412960/04413010.pdf?tp=&isnumber=4412960&arnumber=4413010},
  year = {2007}
}

@inproceedings{TCW+06,
  abstract = {Determining whether a user or system is exercising 
appropriate security practices is difficult in any context. Such 
difficulties are particularly pronounced when uncontrolled or 
unknown platforms join public networks. Commonly practiced 
techniques used to vet these hosts, such as system scans, have 
the potential to infringe upon the privacy of users. In this paper, 
we show that it is possible for clients to prove both the pres- 
ence and proper functioning of security infrastructure without 
allowing unrestricted access to their system. We demonstrate this 
approach, specifically applied to anti-virus security, by requiring 
clients seeking admission to a network to positively identify the 
presence or absence of malcode in a series of puzzles. The 
implementation of this mechanism and its application to real 
networks are also explored. In so doing, we demonstrate that it 
is not necessary for an administrator to be invasive to determine 
whether a client implements good security practices. 
},
  address = {Baltimore, MD},
  author = {Patrick Traynor and Mike Chien and Scott Weaver and Boniface Hicks and Patrick McDaniel},
  booktitle = {Second IEEE Communications Society/CreateNet International Conference on Security and Privacy in Communication Networks (SecureComm '06)},
  date-added = {2007-01-16 16:03:31 -0500},
  date-modified = {2007-01-16 16:32:31 -0500},
  keywords = {Certification, Assurance, Network Security, Malware are totally appropriate and are likely to be observed more Certification, Assurance, Network Security, Malware},
  month = {Aug. 28 - Sep. 1},
  pdf = {papers/traynor-securecomm06antivirus.pdf},
  read = {Yes},
  title = {Non-Invasive Host Certification},
  year = {2006}
}

@inproceedings{HAM06,
  abstract = {Security-typed languages are an evolving tool for implementing
systems with provable security guarantees. However,
to date, these tools have only been used to build simple
"toy" programs. As described in this paper, we have developed
the first real-world, security-typed application: a secure
email system written in the Java language variant Jif.
Real-world policies are mapped onto the information flows
controlled by the language primitives, and we consider the
process and tractability of broadly enforcing security policy
in commodity applications. We find that while the language
provided the rudimentary tools to achieve low-level security
goals, additional tools, services, and language extensions
were necessary to formulate and enforce application
policy. We detail the design and use of these tools. We also
show how the strong guarantees of Jif in conjunction with
our policy tools can be used to evaluate security. This work
serves as a starting point--we have demonstrated that it is
possible to implement real-world systems and policy using
security-typed languages. However, further investigation of
the developer tools and supporting policy infrastructure is
necessary before they can fulfill their considerable promise
of enabling more secure systems.},
  address = {Miami, Fl},
  author = {Boniface Hicks and Kiyan Ahmadizadeh and Patrick McDaniel},
  booktitle = {22st Annual Computer Security Applications Conference (ACSAC)},
  date-added = {2006-09-27 16:30:59 -0400},
  date-modified = {2007-01-16 16:34:12 -0500},
  month = {December},
  note = {Awarded best student paper.},
  pdf = {papers/hicks-acsac06jpmail.pdf},
  title = {Understanding Practical Application Development in Security-typed Languages},
  year = {2006}
}

@inproceedings{HKM+06,
  abstract = {Security-typed languages promise to be a powerful tool with which 
provably secure software applications may be developed. Programs 
written in these languages enforce a strong, global policy of nonin- 
terference which ensures that high-security data will not be observ- 
able on low-security channels. Because noninterference is typically 
too strong a property, most programs use some form of declassifi- 
cation to selectively leak high security information, e.g. when per- 
forming a password check or data encryption. Unfortunately, such 
a declassification is often expressed as an operation within a given 
program, rather than as part of a global policy, making reasoning 
about the security implications of a policy more difficult. 

In this paper, we propose a simple idea we call trusted declas- 
sification in which special declassifier functions are specified as 
part of the global policy. In particular, individual principals declar- 
atively specify which declassifiers they trust so that all informa- 
tion flows implied by the policy can be reasoned about in absence 
of a particular program. We formalize our approach for a Java- 
like language and prove a modified form of noninterference which 
we call noninterference modulo trusted methods. We have imple- 
mented our approach as an extension to Jif and provide some of 
our experience using it to build a secure e-mail client.},
  address = {Ottawa, Canada},
  author = {Boniface Hicks and Dave King and Patrick McDaniel and Michael Hicks},
  booktitle = {Proceedings of the 1st ACM SIGPLAN Workshop on Programming Languages and Analysis for Security ({PLAS} '06)},
  date-modified = {2007-01-16 16:35:24 -0500},
  month = {June 10},
  note = {An extended version of this paper appears in the technical report NAS-TR-0033-2006},
  pdf = {papers/hicks06trustedDeclass.pdf},
  publisher = {ACM Press},
  title = {Trusted Declassification: High-level policy for a security-typed language},
  year = {2006}
}

@inproceedings{FHW96, abstract = {

}, author = {Moreno Falaschi and Patrick Hicks and William H. Winsborough}, booktitle = {Joint International Conference and Symposium on Logic Programming}, note = {An extended version of this paper appears in the Journal of Logic Programming, Vol 41, No. 3, pp 185-215.}, pages = {333-347}, title = {Demand Transformation Analysis for Concurrent Constraint Programs}, url = {citeseer.ist.psu.edu/falaschi94demand.html}, year = {1996} }

@inproceedings{HH98a, abstract = {

}, address = {San Diego, CA}, author = {John Hannan and Patrick Hicks}, booktitle = {Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, month = jan, note = {An extended version of this paper appears in Higher Order and Symbolic Computation, Vol 13, No. 3, 2000, pp 179-216.}, pages = {1--10}, pdf = {papers/HOUncurryingConf.pdf}, title = {Higher-Order Uncurrying}, year = 1998 }

@inproceedings{HH98b,
  abstract = {Arity raising, also known as variable splitting or flattening, is the program optimization which transforms a function of one argument into a function of several arguments by decomposing the structure of the original one argument into individual components in that structure. This optimization eliminates the need for the structuring of the components and also allows more arguments to be passed in registers during a function call. We present a formal specification of arity raising for a higher-order functional language. This specification supports the general arity raising of functions, even for functions which are passed as arguments or returned as values. We define a practical algorithm, based on algorithm W, which implements arity raising, and we prove this algorithm sound with respect to the deductive system. These results provide a declarative framework for reasoning about arity raising and support a richer form of the transformation than is currently found in compilers for functional languages.},
  address = {Baltimore, MD},
  author = {John Hannan and Patrick Hicks},
  booktitle = {Proceedings of 3rd ACM SIGPLAN International Conference on Functional Programming},
  date-modified = {2006-04-03 11:51:21 -0400},
  month = sep,
  pages = {27--38},
  pdf = {papers/HOArityRaising.pdf},
  title = {Higher-Order Arity Raising},
  year = 1998
}

@inproceedings{HWO97,
  abstract = {In this paper, we note and analyze a key trade-off: as the
complexity of caches increases (higher set-associativity, larger
block size, and larger overall size), the power consumed by a
cache access increases. However, because the hit rate also increases,
the number of main memory accesses decreases and
thus the power consumed by a memory access decreases. Recent
papers which consider the power consumption of caches
tend to ignore hit rates. This is unfortunate, because it is
undesirable to have energy-efficient caches which are also
very slow. Hit rates also play a key role in truly evaluating
the energy efficiency of a cache, because low hit rates lead to
more frequent main memory accesses which consume more
power than cache accesses.},
  author = {Patrick Hicks and Matthew Walnock and Robert Michael Owens},
  booktitle = {Proceedings of the 1997 international symposium on Low power electronics and design},
  date-modified = {2005-06-17 11:20:46 -0400},
  doi = {http://doi.acm.org/10.1145/263272.263342},
  isbn = {0-89791-903-3},
  location = {Monterey, California, United States},
  pages = {239--242},
  pdf = {papers/lowpowercaches.pdf},
  publisher = {ACM Press},
  title = {Analysis of power consumption in memory hierarchies},
  year = {1997}
}

@inproceedings{HTH+05, abstract = {

Applications that manipulate sensitive information should ensure end-to-end security by satisfying two properties: sound execution and some form of noninterference. By the former, we mean the program should always perform actions in keeping with its current policy, and by the latter we mean that these actions should never cause high-security information to be visible to a low-security observer. Over the last decade, securitytyped languages have been developed that exhibit these properties, increasingly improving so as to model important features of real programs. No current security-typed language, however, permits general changes to security policies in use by running programs. This paper presents a simple information flow type system for that allows for dynamic security policy updates while ensuring sound execution and a relaxed form of noninterference we term noninterference between updates. We see this work as an important step toward using language-based techniques to ensure end-to-end security for realistic applications.

}, author = {Michael Hicks and Stephen Tse and Boniface Hicks and Steve Zdancewic}, booktitle = {Proceedings of the Foundations of Computer Security Workshop (FCS '05)}, date-modified = {2005-06-17 16:41:39 -0400}, month = {March}, pdf = {papers/dynUpdateInfoflow.pdf}, title = {Dynamic Updating of Information-Flow Policies}, year = 2005 }

Tech Reports

hicks-02-19-08.bib

@techreport{Hic07,
  address = {University Park, PA},
  author = {Boniface Hicks},
  date-added = {2008-02-19 08:20:27 -0500},
  date-modified = {2008-02-19 09:04:35 -0500},
  institution = {Penn State},
  month = {December},
  pdf = {papers/hicks-thesis07secure-systems.pdf},
  school = {Penn State},
  title = {Secure Systems Development Using Security-Typed Languages},
  url = {http://etda.libraries.psu.edu/theses/approved/WorldWideIndex/ETD-2329/index.html},
  year = {2007}
}

@techreport{HRS+07tr,
  address = {Department of Computer Science, Pennsylvania State University},
  author = {Boniface Hicks and Sandra Rueda and St. Clair, Luke and Trent Jaeger and Patrick McDaniel},
  date-added = {2007-01-16 16:02:59 -0500},
  date-modified = {2007-03-15 14:03:51 -0400},
  institution = {Networking and Security Research Center},
  note = {Slightly extended version of SACMAT 2007 publication.},
  number = {NAS-TR-0058-2007},
  title = {A Logical Specification and Analysis for {SELinux} {MLS} Policy},
  year = {2007}
}

@techreport{HRJ+06tr,
  abstract = {Recent advances in security-typed languages and operating system MAC policy have led to a renaissance in information flow security. Grounded in classical security analysis, these technologies provide guarantees preventing data of differing security levels from leaking (confidentiality) or corrupting (integrity) data from other levels. However, these works have largely advanced in isolation. In this paper we investigate the feasibility, design, and cost of unifying the information flow infrastructure at the application, operating system, and network layers. In particular, we develop an infrastructure that enforces a single consistent policy using the information flow controls of the Jif programming language (application), SELinux operating system (OS), and Labeled IPsec (network). We evaluate the security, performance, and complexity of use of the resulting system, and conclude with notes on future directions in the use of these systems. The evaluations and experiments show not only that the overheads are nominal, but that activities such as instrumenting new applications are significantly less cumbersome than in isolated information flow development.
},
  address = {Department of Computer Science and Engineering, Pennsylvania State University, University Park, PA, USA},
  author = {Boniface Hicks and Sandra Rueda and Trent Jaeger and Patrick McDaniel},
  date-added = {2006-09-27 17:23:19 -0400},
  date-modified = {2007-01-16 16:31:01 -0500},
  institution = {Network and Security Research Center},
  month = sep,
  number = {NAS-TR-0049-2006},
  title = {{Breaking Down the Walls of Mutual Distrust: Security-typed Email Using Labeled IPsec}},
  year = 2006
}

@techreport{HKM+06tr,
  abstract = {Security-typed languages promise to be a powerful tool with which provably
  secure software applications may be developed.  Programs written in these
  languages enforce a strong, global policy of noninterference for all their
  data.  Unfortunately, real programs almost always require the use of
  noninterference-violating flows introduced by declassification.  This
  causes the global policy to break down and obscures the meaning of security
  labels.  These languages suffer from the lack of an alternative, global policy
  which can handle declassifications.  In this paper, we present
  a security-typed, object-oriented language which allows
  trusted declassifications based on a global policy.  We prove
  the
  soundness of our language as well as a modified form of noninterference, which
  we call noninterference modulo trusted declassification.  We implement our declassification mechanism and
  global security policy in Jif and provide some examples which motivate its
  use.},
  address = {Department of Computer Science, Pennsylvania State University},
  author = {Boniface Hicks and Dave King and Patrick McDaniel and Michael Hicks},
  date-added = {2006-04-11 10:31:42 -0400},
  date-modified = {2006-09-27 16:50:19 -0400},
  institution = {Networking and Security Research Center},
  month = {March},
  number = {NAS-TR-0033-2006},
  pdf = {papers/hicks06trustedDeclass.pdf},
  title = {Trusted Declassification: High-level policy for a security-typed language},
  year = {2006}
}

@techreport{HKM05,
  abstract = {Security-typed languages are powerful tools for provably enforcing
noninterference.
Real computing systems, however, often intentionally violate
noninterference by deliberately releasing (or declassifying) sensitive
information.
These systems frequently trust cryptographic functions to achieve
declassification while still maintaining confidentiality.
We introduce the notion of trusted functions that implicitly act as
declassifiers within a security-typed language.
Proofs of the new language's soundness and its enforcement of a
weakened form of noninterference are given.
Additionally, we implement trusted functions used for declassification
in the Jif language.
This represents a step forward in making security-typed languages more
practical for use in real systems.},
  address = {Department of Computer Science, Pennsylvania State University},
  author = {Boniface Hicks and Dave King and Patrick McDaniel},
  institution = {Network and Security Center},
  month = {January},
  note = {({\it updated May 2005})},
  number = {NAS-TR-0004-2005},
  pdf = {papers/TechReport-0004-2004.pdf},
  title = {{Declassification with Cryptographic Functions in a Security-Typed Language}},
  year = {2005}
}

@techreport{HMH05, abstract = {

Because of the increasing demands for privacy and integrity guarantees in applications that handle sensitive, electronic data, there is a need for automated software development tools and techniques for enforcing this security. Although there have been many attempts to apply security to existing systems after the fact, manifold failures indicate that this approach should be revisited. To the contrary, experience indicates that secure systems must be designed with explicit policies from the beginning and that there should be some automated, mathematically-verifiable mechanism to aid programmers in doing this correctly. Recent research in language-based security has made great strides towards the development of sophisticated and robust languages for programming with explicit security policies. Insufficient experience with these languages, however, has left them untested and impractical for writing real, distributed applications. In this paper, we present our experiences of working with Jif, a Java-based, security-typed language, in building a distributed, database application. Our experience has indicated the current impracticality of programming in Jif, but has helped us to identify language development tools and automation algorithms that could aid in making Jif more practical for developing real, distributed applications.

}, address = {Department of Computer Science, Pennsylvania State University}, author = {Boniface Hicks and Patrick McDaniel and Ali Hurson}, institution = {Network and Security Center}, month = {April}, number = {NAS-TR-0011-2005}, pdf = {papers/hicks05tr0011-2005.pdf}, title = {Information Flow Control in Database Security: A Case Study for Secure Programming with Jif}, year = {2005} }