• Jif

  • Referenced in 16 articles [sw16478]
  • Java information flow. Jif is a security-typed programming language that extends Java with support...
  • Miranda

  • Referenced in 152 articles [sw04986]
  • documented programming languages. Miranda is a functional programming language which has been developed with this ... polymorphic type system and (ii) a library structure with type secure facilities for separate compilation ... type system and in particular the facilities for userdefined types in Miranda, with other aspects ... language and its programming environment being only briefly sketched...
  • F*

  • Referenced in 19 articles [sw27563]
  • proof assistant based on dependent types. After verification, F* programs can be extracted to efficient ... This enables verifying the functional correctness and security of realistic applications. The main ongoing ... primitives. F*’s type system includes dependent types, monadic effects, refinement types, and a weakest ... specifications for programs, including functional correctness and security properties. The F* type-checker aims...
  • Aglet

  • Referenced in 4 articles [sw13305]
  • Security-typed programming within dependently typed programming. Several recent security-typed programming languages, such ... this paper, we show that security-typed programming can be embedded as a library within ... major features of existing security-typed programming languages, such as decentralized access control, typed proof...
  • gmp

  • Referenced in 265 articles [sw00363]
  • cryptography applications and research, Internet security applications, algebra systems, computational algebra research ... using fullwords as the basic arithmetic type, by using fast algorithms, with highly optimised assembly ... restrictions on the use with non-free programs. GMP is part of the GNU project...
  • Flow Caml

  • Referenced in 6 articles [sw08923]
  • basically to allow to write ”real” programs and to automatically check that they obey some ... Flow Caml, standard ML types are annotated with security levels chosen in a user-definable ... analyzed program is legal with regard to the security policy specified by the programmer. Technically ... size implementations of a programming language equipped with a type system that features simultaneously subtyping...
  • TS#

  • Referenced in 3 articles [sw14208]
  • type systems, TS# features full runtime reflection over three kinds of types: (1) simple types ... type any, for dynamically type-safe TS# expressions; and (3) the type un, for untrusted ... embedded. After type-checking, the compiler instruments the program with various checks to ensure ... examples illustrate how web security patterns that developers currently program in JavaScript (with much difficulty...
  • Laminar

  • Referenced in 3 articles [sw23077]
  • promising model for writing programs with powerful, end-to-end security guarantees. Current DIFC systems ... data in lexically scoped security regions. Laminar enforces the security policies specified by the labels ... security module. This paper shows that security regions ease incremental deployment and limit dynamic security ... DIFC systems only support limited types of multithreaded programs, Laminar supports a more general class...
  • LaCasa

  • Referenced in 2 articles [sw34853]
  • most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation ... widely-used in program security. We formalize our approach as a type system and prove...
  • LIFT

  • Referenced in 3 articles [sw20596]
  • technique to detect a wide range of security attacks. However, current information flow tracking systems ... very practical, because they either require program annotations, source code, non-trivial hardware extensions ... instrumentation and optimizations for detecting various types of security attacks without requiring any hardware changes ... that LIFT can effectively detect various types of security attacks. LIFT also incurs very...
  • MetaKlaim

  • Referenced in 5 articles [sw01810]
  • MetaKlaim: a type safe multi-stage language for global computing This paper describes the design ... extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction ... programming activities (such as assembly and linking of code fragments), dynamic checking of security policies ... code mobility). MetaKlaim exploits a powerful type system (including polymorphic types à la system...
  • Celf

  • Referenced in 2 articles [sw22718]
  • systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics ... Celf is an implementation of the CLF type ... theory that extends the LF type theory by linear types to support representation of state ... types methodology for specification and the interpretation of CLF signatures as concurrent logic programs...
  • GREMLIN

  • Referenced in 5 articles [sw03276]
  • structure program GREMLIN in a very heterogeneous SSH-connected WAN-cluster of UNIX-type hosts ... cluster via PVM 3.4.3. The secure shell protocol is used for connection and communication purposes ... initial benchmark run with the Hartree Fock program GREMLIN reveals a speed difference of roughly...
  • RADA

  • Referenced in 4 articles [sw20732]
  • reasoning about recursive programs that manipulate algebraic types. RADA operates by successively unrolling catamorphisms ... messages should be allowed to cross network security domains. Promising experimental results demonstrate that RADA...
  • MinX

  • Referenced in 2 articles [sw18523]
  • recursive datatypes. Reconstructing the meaning of a program from its binary executable is known ... wide range of applications in software security, exposing piracy, legacy systems, etc. Since reversing ... there is much interest in inferring a type (a meaning) for the elements ... reconstructed types. Key to our approach is the derivation of a witness program...
  • MinC

  • Referenced in 2 articles [sw18524]
  • recursive datatypes. Reconstructing the meaning of a program from its binary executable is known ... wide range of applications in software security, exposing piracy, legacy systems, etc. Since reversing ... there is much interest in inferring a type (a meaning) for the elements ... reconstructed types. Key to our approach is the derivation of a witness program...
  • Pixy

  • Referenced in 5 articles [sw25249]
  • same time, the quantity and impact of security vulnerabilities in such applications have grown ... analysis to discover vulnerable points in a program. In addition, alias and literal analysis ... applied to the detection of vulnerability types such as SQL injection, cross-site scripting ... therefore, low enough to permit effective security audits...
  • Merlin

  • Referenced in 3 articles [sw23076]
  • finding security violations that are caused by explicit information flow in programs. Much of this ... vulnerabilities such as buffer overruns common in type-unsafe languages such ... automatically inferring explicit information flow specifications from program code. Such specifications greatly reduce manual labor ... results, while using tools that check for security violations caused by explicit information flow. Beginning...
  • Volpano Smith

  • Referenced in 1 article [sw29543]
  • Volpano/Smith Security Typing System. The Volpano/Smith/Irvine security type systems requires that variables are annotated ... high (secret) or low (public), and provides typing rules which guarantee that secret values cannot ... public output ports. This property of a program is called confidentiality. For a simple while...
  • ModuleML

  • Referenced in 1 article [sw16987]
  • compiler compiles whole programs. This paper presents a compilation scheme that securely compiles a standalone ... into untyped assembly. The compilation scheme is secure in that it reflects the abstractions ... level memory isolation mechanism and by dynamically type checking its interactions. We evaluate an implementation...