• Gem #83: Type-Based Security 2: Validating the Input

    Ada Gem #83 — Ada's strong type system makes it quite convenient to check at compilation time that certain security properties are verified, for example that a tainted value is not used where a trusted one is expected, or that data is properly validated before being used in a sensitive context (think of SQL injection attacks).
    In the first Gem of this series of two, we discussed how to handle tainted data. In this Gem, we explain how to validate the input given to an SQL command. (For an amusing comic-strip description of what SQL injection is, see: http://xkcd.com/327/.) Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #82: Type-Based Security 1: Handling Tainted Data

    Ada Gem #82 — The strong type system in Ada makes it quite convenient to check at compile time that certain security properties are verified, for example that a tainted value is not used where a trusted one is expected, or that data is properly validated before being used in a sensitive context (think of SQL injection attacks).
    In this series of two Gems, we present short examples of how this might be done. The first Gem discusses how to handle tainted data. Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #80: Speedy Shift and Rotate in SPARK

    Ada Gem #80 — This Gem covers a topic that I recently encountered while working on a crypto algorithm in SPARK: how to use Ada's predefined shift and rotate functions with modular types from a SPARK program. Continue Reading »

    Rod Chapman
    Altran
  • Gem #76: Tokeneer Discovery - Lesson 6

    Ada Gem #76 — In the previous Gem in this series, we saw how to deal with overflow errors, based on source code from Tokeneer. In this Gem, we show how to ensure secure information flow.
    This Gem brings us to the end of this series on Tokeneer, and we would like to say a big thank you to the SPARK team at Altran for providing these resources.
    We will now take a break for the holiday period and will return with more Gems on January 11, 2010. Very happy holidays to all Gem readers, wherever you are!
    Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #75: Tokeneer Discovery - Lesson 5

    Ada Gem #75 — In the previous Gem in this series, we saw how the SPARK Toolset can verify application-specific safety and security properties, based on source code from Tokeneer. In this Gem, we show how to deal with overflow errors. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #74: Tokeneer Discovery - Lesson 4

    Ada Gem #74 — In the previous Gem in this series, we saw how to validate input in SPARK, based on source code from Tokeneer. In this Gem, we show how the SPARK Toolset can verify application-specific safety and security properties. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #73: Tokeneer Discovery - Lesson 3

    Ada Gem #73 — In the previous Gem in this series, we saw how to identify ineffective statements in SPARK, based on source code from Tokeneer. In this Gem, we show how to validate input. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #72: Tokeneer Discovery - Lesson 2

    Ada Gem #72 — In the previous Gem in this series we saw how to deal with improper initialization in SPARK, based on source code from Tokeneer. In this Gem, we show how to identify ineffective statements. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #71: Tokeneer Discovery - Lesson 1

    Ada Gem #71 — In previous Gems, we saw how to create a SPARK project in GPS, and how to run the Examiner and Simplifier tools to verify various properties of a simple linear search function. In this series of Gems on SPARK, we will explore SPARK capabilities in greater depth, using source code from Tokeneer, an NSA-funded, highly secure biometric software system.
    In this Gem, we show how to deal with improper initialization. Continue Reading »

    Dean Kuo, Angela Wallenburg
  • Gem #69: Let's SPARK! - Part 2

    Ada Gem #69 — Welcome back! We hope you had a great summer. Now let's get back to where we left off.
    In this Gem and the previous one, we give you a simple walkthrough of SPARK's capabilities and its integration with GPS. In the previous Gem, we showed how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors. In this Gem, we show how to prove that your SPARK programs respect given contracts. Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #68: Let's SPARK! - Part 1

    Ada Gem #68 — Please note that this is the final Gem before we break for summer. The series will resume on September 7, 2009.

    In this Gem and the next one, we present a simple walk-through of SPARK's capabilities and its integration with GPS. In this first Gem, we show how to set up a SPARK project and prove that your SPARK programs are free from uninitialized variable accesses and that they execute without run-time errors.

    Continue Reading »

    Yannick Moy
    AdaCore
  • Gem #53: Safe and Secure Software: Chapter 12: Conclusion

    Gem #53 is the concluding chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    We hope you have enjoyed this series. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #51: Safe and Secure Software: Chapter 11, Certified Safe with SPARK

    Gem #51 is the eleventh chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #49: Safe and Secure Software: Chapter 10, Safe Concurrency

    Gem #49 is the tenth chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #47: Safe and Secure Software : Chapter 9, Safe Communication

    Gem #47 is the ninth chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #45: Safe and Secure Software : Chapter 8, Safe Startup

    Gem #45 is the eighth chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #43: Safe and Secure Software : Chapter 7, Safe Memory Management

    Welcome back the Ada Gems series! We hope you had a great summer.

    Gem #43 is the seventh chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    Continue Reading »

    John Barnes
  • Gem #42: Safe and Secure Software : Chapter 6, Safe Object Construction

    Welcome to the final gem before we take a break for the summer, which is the sixth chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet.

    The gems series will recommence in September. In the meantime, we hope you have a wonderful summer!

    Continue Reading »

    John Barnes
  • Gem #40: Safe and Secure Software : Chapter 5, Safe Object Oriented Programming

    This week's gem is the fifth chapter of John Barnes' new booklet:

    Safe and Secure Software: An Introduction to Ada 2005.

    Over the coming months, we will be publishing all thirteen chapters of the booklet. In the attachment at the bottom of Gem #30 you can access the contents and bibliography for the entire booklet. We hope you will enjoy the read!

    Continue Reading »

    John Barnes
  • Gem #39: Efficient Stream I/O for Array Types

    Ada Gem #39 — Reading and writing values from/to streams is easy with Ada’s “stream attributes” but for some array types the default attribute implementations could be made more efficient. In this Gem we show how the user can define these more efficient implementations. Continue Reading »

    Pat Rogers
    AdaCore
   1  2     Next »